diff --git a/heapster-saw/examples/arrays.sawcore b/heapster-saw/examples/arrays.sawcore
index 6b1f16867b..50d9eaa081 100644
--- a/heapster-saw/examples/arrays.sawcore
+++ b/heapster-saw/examples/arrays.sawcore
@@ -8,34 +8,34 @@ import Prelude;
 -- noErrorsContains0H len i v =
 --   orM (exists x. returnM x) (noErrorsContains0H len (i+1) v)
 noErrorsContains0H : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
-                     CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool);
+                     CompM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool);
 noErrorsContains0H len_top i_top v_top =
   letRecM
     (LRT_Cons
      (LRT_Fun (Vec 64 Bool) (\ (len:Vec 64 Bool) ->
       LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) ->
       LRT_Fun (BVVec 64 len (Vec 64 Bool)) (\ (_:BVVec 64 len (Vec 64 Bool)) ->
-      LRT_Ret (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)))))
+      LRT_Ret #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)))))
      LRT_Nil)
-    (BVVec 64 len_top (Vec 64 Bool) * Vec 64 Bool)
+    #(BVVec 64 len_top (Vec 64 Bool), Vec 64 Bool)
     (\ (f : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
-            CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)) ->
+            CompM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)) ->
        ((\ (len:Vec 64 Bool) (i:Vec 64 Bool) (v:BVVec 64 len (Vec 64 Bool)) ->
            precondHint
-             (CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool))
+             (CompM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool))
              (and (bvsle 64 0x0000000000000000 i)
                   (bvsle 64 i 0x0fffffffffffffff))
-             (orM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
-                  (existsM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
-                           (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
-                           (returnM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)))
+             (orM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)
+                  (existsM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)
+                           #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)
+                           (returnM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)))
                   (f len (bvAdd 64 i 0x0000000000000001) v))), ()))
     (\ (f : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
-            CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)) ->
+            CompM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)) ->
        f len_top i_top v_top);
 
 -- The specification that contains0 has no errors
 noErrorsContains0 : (len:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
-                    CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool);
+                    CompM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool);
 noErrorsContains0 len v =
   noErrorsContains0H len 0x0000000000000000 v;
diff --git a/heapster-saw/examples/clearbufs.sawcore b/heapster-saw/examples/clearbufs.sawcore
index 794f9a00bf..d3326aba19 100644
--- a/heapster-saw/examples/clearbufs.sawcore
+++ b/heapster-saw/examples/clearbufs.sawcore
@@ -25,28 +25,28 @@ Mbox_def = Mbox;
             (m:Mbox) -> P m;
 Mbox__rec P f1 f2 m = Mbox#rec P f1 f2 m; -}
 
---unfoldMbox : Mbox -> Either #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool));
+--unfoldMbox : Mbox -> Either #() #(Mbox, Vec 64 Bool, BVVec 64 bv64_16 (Vec 64 Bool));
 primitive
-unfoldMbox : Mbox -> Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 len (Vec 64 Bool)));
+unfoldMbox : Mbox -> Either #() (Sigma (V64) (\ (len : V64) -> #(Mbox, BVVec 64 len (Vec 64 Bool))));
 
 {-unfoldMbox m =
-  Mbox__rec (\ (_:Mbox) -> Either #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool) * #()))
-  (Left #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool) * #()) ())
-  (\ (m:Mbox) (_:Either #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool) * #())) (len:Vec 64 Bool) (d:BVVec 64 bv64_16 (Vec 64 Bool)) ->
-     Right #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool) * #()) (m, len, d, ()))
+  Mbox__rec (\ (_:Mbox) -> Either #() #(Mbox, Vec 64 Bool, BVVec 64 bv64_16 (Vec 64 Bool), #()))
+  (Left #() #(Mbox, Vec 64 Bool, BVVec 64 bv64_16 (Vec 64 Bool), #()) ())
+  (\ (m:Mbox) (_:Either #() #(Mbox, Vec 64 Bool, BVVec 64 bv64_16 (Vec 64 Bool), #())) (len:Vec 64 Bool) (d:BVVec 64 bv64_16 (Vec 64 Bool)) ->
+     Right #() #(Mbox, Vec 64 Bool, BVVec 64 bv64_16 (Vec 64 Bool), #()) (m, len, d, ()))
   m;
   -}
 
 primitive
-foldMbox : Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 len (Vec 64 Bool))) -> Mbox;
+foldMbox : Either #() (Sigma (V64) (\ (len : V64) -> #(Mbox, BVVec 64 len (Vec 64 Bool)))) -> Mbox;
 
---(Mbox * Vec 64 Bool * (BVVec 64 bv64_16 (Vec 64 Bool)) * #()) -> Mbox;
+--#(Mbox, Vec 64 Bool, (BVVec 64 bv64_16 (Vec 64 Bool)), #()) -> Mbox;
 {-
 foldMbox =
-  either #() (Mbox * Vec 64 Bool * (BVVec 64 bv64_16 (Vec 64 Bool)) * #()) Mbox
+  either #() #(Mbox, Vec 64 Bool, (BVVec 64 bv64_16 (Vec 64 Bool)), #()) Mbox
          (\ (_:#()) -> Mbox_nil)
-         (\ (tup : (Mbox * Vec 64 Bool * (BVVec 64 bv64_16 (Vec 64 Bool)) * #())) ->
-            Mbox_cons tup.1 tup.2 tup.3);
+         (\ (tup : #(Mbox, Vec 64 Bool, (BVVec 64 bv64_16 (Vec 64 Bool)), #())) ->
+            Mbox_cons tup.0 tup.1 tup.2);
 			-}
 
 primitive
diff --git a/heapster-saw/examples/global_var.sawcore b/heapster-saw/examples/global_var.sawcore
index a1f63d7f19..eade3439b1 100644
--- a/heapster-saw/examples/global_var.sawcore
+++ b/heapster-saw/examples/global_var.sawcore
@@ -2,8 +2,8 @@ module GlobalVar where
 
 import Prelude;
 
-acquireLockM : Vec 64 Bool -> CompM (Vec 64 Bool * Vec 64 Bool);
-acquireLockM u = returnM (Vec 64 Bool * Vec 64 Bool)
+acquireLockM : Vec 64 Bool -> CompM #(Vec 64 Bool, Vec 64 Bool);
+acquireLockM u = returnM #(Vec 64 Bool, Vec 64 Bool)
 			 (u,u);
 
 releaseLockM : Vec 64 Bool -> Vec 64 Bool -> CompM (Vec 64 Bool);
diff --git a/heapster-saw/examples/iter_linked_list.sawcore b/heapster-saw/examples/iter_linked_list.sawcore
index fbb59e816b..421650dbc6 100644
--- a/heapster-saw/examples/iter_linked_list.sawcore
+++ b/heapster-saw/examples/iter_linked_list.sawcore
@@ -27,20 +27,20 @@ ListF__rec : (a b:sort 0) -> (P : ListF a b -> sort 0) ->
              (l:ListF a b) -> P l;
 ListF__rec a b P f1 f2 l = ListF#rec a b P f1 f2 l;
 
-unfoldListF : (a b:sort 0) -> ListF a b -> Either b (a * ListF a b);
+unfoldListF : (a b:sort 0) -> ListF a b -> Either b #(a, ListF a b);
 unfoldListF a b l =
-  ListF__rec a b (\ (_:ListF a b) -> Either b (a * ListF a b))
-  (\ (x:b) -> Left b (a * ListF a b) x)
-  (\ (x:a) (l:ListF a b) (_:Either b (a * ListF a b)) ->
-     Right b (a * ListF a b) (x, l))
+  ListF__rec a b (\ (_:ListF a b) -> Either b #(a, ListF a b))
+  (\ (x:b) -> Left b #(a, ListF a b) x)
+  (\ (x:a) (l:ListF a b) (_:Either b #(a, ListF a b)) ->
+     Right b #(a, ListF a b) (x, l))
   l;
 
-foldListF : (a b:sort 0) -> Either b (a * ListF a b) -> ListF a b;
+foldListF : (a b:sort 0) -> Either b #(a, ListF a b) -> ListF a b;
 foldListF a b =
-  either b (a * ListF a b) (ListF a b)
+  either b #(a, ListF a b) (ListF a b)
          (\ (x : b) -> NilF a b x)
-         (\ (tup : (a * ListF a b)) ->
-            ConsF a b tup.(1) tup.(2));
+         (\ (tup : #(a, ListF a b)) ->
+            ConsF a b tup.0 tup.1);
 
 getListF : (a b:sort 0) -> ListF a b -> b;
 getListF a b =
diff --git a/heapster-saw/examples/mbox.sawcore b/heapster-saw/examples/mbox.sawcore
index 0b751a6be9..86f6a30812 100644
--- a/heapster-saw/examples/mbox.sawcore
+++ b/heapster-saw/examples/mbox.sawcore
@@ -31,20 +31,20 @@ Mbox__rec : (P : Mbox -> sort 0) ->
             (m:Mbox) -> P m;
 Mbox__rec P f1 f2 m = Mbox#rec P f1 f2 m;
 
-unfoldMbox : Mbox -> Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool));
+unfoldMbox : Mbox -> Either #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool));
 unfoldMbox m =
-  Mbox__rec (\ (_:Mbox) -> Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)))
-  (Left #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) ())
-  (\ (strt:Vec 64 Bool) (len:Vec 64 Bool) (m:Mbox) (_:Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool))) (d:BVVec 64 bv64_128 (Vec 8 Bool)) ->
-     Right #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) (strt, len, m, d))
+  Mbox__rec (\ (_:Mbox) -> Either #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool)))
+  (Left #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool)) ())
+  (\ (strt:Vec 64 Bool) (len:Vec 64 Bool) (m:Mbox) (_:Either #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool))) (d:BVVec 64 bv64_128 (Vec 8 Bool)) ->
+     Right #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool)) (strt, len, m, d))
   m;
 
-foldMbox : Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) -> Mbox;
+foldMbox : Either #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool)) -> Mbox;
 foldMbox =
-  either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) Mbox
+  either #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool)) Mbox
          (\ (_:#()) -> Mbox_nil)
-         (\ (tup : (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool))) ->
-            Mbox_cons tup.1 tup.2 tup.3 tup.(2).(2).(2));
+         (\ (tup : #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool))) ->
+            Mbox_cons tup.0 tup.1 tup.2 tup.3);
 
 {-
 getMbox : (a : sort 0) -> Mbox a -> a;
diff --git a/heapster-saw/examples/rust_data.sawcore b/heapster-saw/examples/rust_data.sawcore
index 9d39cde030..79da911517 100644
--- a/heapster-saw/examples/rust_data.sawcore
+++ b/heapster-saw/examples/rust_data.sawcore
@@ -3,17 +3,17 @@ module rust_data where
 
 import Prelude;
 
-unfoldListPermH : (a:sort 0) -> List a -> Either #() (#() * a * List a);
+unfoldListPermH : (a:sort 0) -> List a -> Either #() #(#(), a, List a);
 unfoldListPermH a l =
-  List__rec a (\ (_:List a) -> Either #() (#() * a * List a))
-  (Left #() (#() * a * List a) ())
-  (\ (x:a) (l:List a) (_:Either #() (#() * a * List a)) ->
-     Right #() (#() * a * List a) ((), x, l))
+  List__rec a (\ (_:List a) -> Either #() #(#(), a, List a))
+  (Left #() #(#(), a, List a) ())
+  (\ (x:a) (l:List a) (_:Either #() #(#(), a, List a)) ->
+     Right #() #(#(), a, List a) ((), x, l))
   l;
 
-foldListPermH : (a:sort 0) -> Either #() (#() * a * List a) -> List a;
+foldListPermH : (a:sort 0) -> Either #() #(#(), a, List a) -> List a;
 foldListPermH a =
-  either #() (#() * a * List a) (List a)
+  either #() #(#(), a, List a) (List a)
          (\ (_ : #()) -> Nil a)
-         (\ (tup : (#() * a * List a)) ->
-            Cons a tup.(2).(1) tup.(2).(2));
+         (\ (tup : #(#(), a, List a)) ->
+            Cons a tup.(1) tup.(2));
diff --git a/heapster-saw/examples/rust_lifetimes.sawcore b/heapster-saw/examples/rust_lifetimes.sawcore
index ea6aa76bf6..30b958f89f 100644
--- a/heapster-saw/examples/rust_lifetimes.sawcore
+++ b/heapster-saw/examples/rust_lifetimes.sawcore
@@ -3,17 +3,17 @@ module rust_lifetimes where
 
 import Prelude;
 
-unfoldListPermH : (a:sort 0) -> List a -> Either #() (#() * a * List a);
+unfoldListPermH : (a:sort 0) -> List a -> Either #() #(#(), a, List a);
 unfoldListPermH a l =
-  List__rec a (\ (_:List a) -> Either #() (#() * a * List a))
-  (Left #() (#() * a * List a) ())
-  (\ (x:a) (l:List a) (_:Either #() (#() * a * List a)) ->
-     Right #() (#() * a * List a) ((), x, l))
+  List__rec a (\ (_:List a) -> Either #() #(#(), a, List a))
+  (Left #() #(#(), a, List a) ())
+  (\ (x:a) (l:List a) (_:Either #() #(#(), a, List a)) ->
+     Right #() #(#(), a, List a) ((), x, l))
   l;
 
-foldListPermH : (a:sort 0) -> Either #() (#() * a * List a) -> List a;
+foldListPermH : (a:sort 0) -> Either #() #(#(), a, List a) -> List a;
 foldListPermH a =
-  either #() (#() * a * List a) (List a)
+  either #() #(#(), a, List a) (List a)
          (\ (_ : #()) -> Nil a)
-         (\ (tup : (#() * a * List a)) ->
-            Cons a tup.(2).(1) tup.(2).(2));
+         (\ (tup : #(#(), a, List a)) ->
+            Cons a tup.(1) tup.(2));
diff --git a/heapster-saw/examples/string_set.sawcore b/heapster-saw/examples/string_set.sawcore
index ebb12ebe76..e22d5c4520 100644
--- a/heapster-saw/examples/string_set.sawcore
+++ b/heapster-saw/examples/string_set.sawcore
@@ -8,10 +8,10 @@ listInsertM a l s =
   returnM (List a) (Cons a s l);
 
 listRemoveM : (a : sort 0) -> (a -> a -> Bool) -> List a -> a ->
-              CompM (List a * a);
+              CompM #(List a, a);
 listRemoveM a test_eq l s =
   returnM
-    (List a * a)
+    #(List a, a)
     (List__rec
       a (\ (_:List a) -> List a)
       (Nil a)
@@ -30,10 +30,10 @@ stringListInsertM : List String -> String -> CompM (List String);
 stringListInsertM l s =
   returnM (List String) (Cons String s l);
 
-stringListRemoveM : List String -> String -> CompM (stringList * String);
+stringListRemoveM : List String -> String -> CompM #(stringList, String);
 stringListRemoveM l s =
   returnM
-    (stringList * String)
+    #(stringList, String)
     (List__rec
       String (\ (_:List String) -> List String)
       (Nil String)