src/Pure/proofterm.ML

--- a/src/Pure/proofterm.ML	Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/proofterm.ML	Thu May 31 23:47:36 2007 +0200
@@ -250,7 +250,7 @@
       (PThm (_, prf', _, _), _) => prf'
     | _ => prf);
 
-val mk_Abst = foldr (fn ((s, T:typ), prf) => Abst (s, NONE, prf));
+val mk_Abst = fold_rev (fn (s, T:typ) => fn prf => Abst (s, NONE, prf));
 fun mk_AbsP (i, prf) = funpow i (fn prf => AbsP ("H", NONE, prf)) prf;
 
 fun apsome f NONE = raise SAME
@@ -621,7 +621,7 @@
   let
     val used = it_term_types add_typ_tfree_names (t, [])
     and tvars = map #1 (it_term_types add_typ_tvars (t, []));
-    val (alist, _) = foldr new_name ([], used) tvars;
+    val (alist, _) = List.foldr new_name ([], used) tvars;
   in
     (case alist of
       [] => prf (*nothing to do!*)
@@ -643,9 +643,9 @@
     val j = length Bs;
   in
     mk_AbsP (j+1, proof_combP (prf, map PBound
-      (j downto 1) @ [mk_Abst (mk_AbsP (i,
+      (j downto 1) @ [mk_Abst params (mk_AbsP (i,
         proof_combP (proof_combt (PBound i, map Bound ((length params - 1) downto 0)),
-          map PBound (((i-m-1) downto 0) @ ((i-1) downto (i-m)))))) params]))
+          map PBound (((i-m-1) downto 0) @ ((i-1) downto (i-m))))))]))
   end;
 
 
@@ -700,7 +700,7 @@
     val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop);
     val k = length ps;
 
-    fun mk_app (b, (i, j, prf)) =
+    fun mk_app b (i, j, prf) =
           if b then (i-1, j, prf %% PBound i) else (i, j-1, prf %> Bound j);
 
     fun lift Us bs i j (Const ("==>", _) $ A $ B) =
@@ -708,7 +708,7 @@
       | lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) =
             Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t)
       | lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf,
-            map (fn k => (#3 (foldr mk_app (i-1, j-1, PBound k) bs)))
+            map (fn k => (#3 (fold_rev mk_app bs (i-1, j-1, PBound k))))
               (i + k - 1 downto i));
   in
     mk_AbsP (k, lift [] [] 0 0 Bi)
@@ -1200,7 +1200,7 @@
       map SOME (sort Term.term_ord (term_frees prop));
     val opt_prf = if ! proofs = 2 then
         #4 (shrink_proof thy [] 0 (rewrite_prf fst (ProofData.get thy)
-          (foldr (uncurry implies_intr_proof) prf hyps)))
+          (fold_rev implies_intr_proof hyps prf)))
       else MinProof (mk_min_proof prf ([], [], []));
     val head = (case strip_combt (fst (strip_combP prf)) of
         (PThm (old_name, prf', prop', NONE), args') =>