src/Pure/tctical.ML

 
 (*Apply every tactic to 1*)
 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;
 
 (*Apply tactics on consecutive subgoals*)

 in
 
 (*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
       val (params,hyps,concl) = strip_context prem'
   in (insts,params,hyps,concl)  end;

       fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
       (*A form of lifting that discharges assumptions.*)
       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
             val emBs = map (cterm o embed) (prems_of st')
             val Cth  = implies_elim_list st' (map (elim o assume) emBs)