src/Provers/splitter.ML

--- a/src/Provers/splitter.ML	Tue Oct 27 22:55:27 2009 +0100
+++ b/src/Provers/splitter.ML	Tue Oct 27 22:56:14 2009 +0100
@@ -151,7 +151,7 @@
 
 
 (* add all loose bound variables in t to list is *)
-fun add_lbnos (is,t) = add_loose_bnos (t,0,is);
+fun add_lbnos t is = add_loose_bnos (t, 0, is);
 
 (* check if the innermost abstraction that needs to be removed
    has a body of type T; otherwise the expansion thm will fail later on
@@ -191,7 +191,7 @@
 fun mk_split_pack (thm, T: typ, T', n, ts, apsns, pos, TB, t) =
   if n > length ts then []
   else let val lev = length apsns
-           val lbnos = Library.foldl add_lbnos ([],Library.take(n,ts))
+           val lbnos = fold add_lbnos (Library.take (n, ts)) []
            val flbnos = List.filter (fn i => i < lev) lbnos
            val tt = incr_boundvars (~lev) t
        in if null flbnos then
@@ -253,20 +253,21 @@
       | posns Ts pos apsns t =
           let
             val (h, ts) = strip_comb t
-            fun iter((i, a), t) = (i+1, (posns Ts (i::pos) apsns t) @ a);
-            val a = case h of
-              Const(c, cT) =>
-                let fun find [] = []
-                      | find ((gcT, pat, thm, T, n)::tups) =
-                          let val t2 = list_comb (h, Library.take (n, ts))
-                          in if Sign.typ_instance sg (cT, gcT)
-                                andalso fomatch sg (Ts,pat,t2)
-                             then mk_split_pack(thm,T,T',n,ts,apsns,pos,type_of1(Ts,t2),t2)
-                             else find tups
-                          end
-                in find (these (AList.lookup (op =) cmap c)) end
-            | _ => []
-          in snd(Library.foldl iter ((0, a), ts)) end
+            fun iter t (i, a) = (i+1, (posns Ts (i::pos) apsns t) @ a);
+            val a =
+              case h of
+                Const(c, cT) =>
+                  let fun find [] = []
+                        | find ((gcT, pat, thm, T, n)::tups) =
+                            let val t2 = list_comb (h, Library.take (n, ts))
+                            in if Sign.typ_instance sg (cT, gcT)
+                                  andalso fomatch sg (Ts,pat,t2)
+                               then mk_split_pack(thm,T,T',n,ts,apsns,pos,type_of1(Ts,t2),t2)
+                               else find tups
+                            end
+                  in find (these (AList.lookup (op =) cmap c)) end
+              | _ => []
+          in snd (fold iter ts (0, a)) end
   in posns Ts [] [] t end;
 
 fun nth_subgoal i thm = List.nth (prems_of thm, i-1);
@@ -336,8 +337,8 @@
       (Logic.strip_assums_concl (Thm.prop_of thm'))));
     val cert = cterm_of (Thm.theory_of_thm state);
     val cntxt = mk_cntxt_splitthm t tt TB;
-    val abss = Library.foldl (fn (t, T) => Abs ("", T, t));
-  in cterm_instantiate [(cert P, cert (abss (cntxt, Ts)))] thm'
+    val abss = fold (fn T => fn t => Abs ("", T, t));
+  in cterm_instantiate [(cert P, cert (abss Ts cntxt))] thm'
   end;