--- a/src/Pure/tctical.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/tctical.ML Thu May 31 23:47:36 2007 +0200
@@ -177,10 +177,10 @@
fun EVERY1 tacs = EVERY' tacs 1;
(* FIRST [tac1,...,tacn] equals tac1 ORELSE ... ORELSE tacn *)
-fun FIRST tacs = foldr (op ORELSE) no_tac tacs;
+fun FIRST tacs = fold_rev (curry op ORELSE) tacs no_tac;
(* FIRST' [tac1,...,tacn] i equals tac1 i ORELSE ... ORELSE tacn i *)
-fun FIRST' tacs = foldr (op ORELSE') (K no_tac) tacs;
+fun FIRST' tacs = fold_rev (curry op ORELSE') tacs (K no_tac);
(*Apply first tactic to 1*)
fun FIRST1 tacs = FIRST' tacs 1;
@@ -413,7 +413,7 @@
(*Common code for METAHYPS and metahyps_thms*)
fun metahyps_split_prem prem =
let (*find all vars in the hyps -- should find tvars also!*)
- val hyps_vars = foldr add_term_vars [] (Logic.strip_assums_hyp prem)
+ val hyps_vars = List.foldr add_term_vars [] (Logic.strip_assums_hyp prem)
val insts = map mk_inst hyps_vars
(*replace the hyps_vars by Frees*)
val prem' = subst_atomic insts prem
@@ -453,7 +453,7 @@
fun relift st =
let val prop = Thm.prop_of st
val subgoal_vars = (*Vars introduced in the subgoals*)
- foldr add_term_vars [] (Logic.strip_imp_prems prop)
+ List.foldr add_term_vars [] (Logic.strip_imp_prems prop)
and concl_vars = add_term_vars (Logic.strip_imp_concl prop, [])
val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st