src/Pure/tctical.ML
changeset 23178 07ba6b58b3d2
parent 23139 aa899bce7c3b
child 23224 e9fb2ff046fc
     1.1 --- a/src/Pure/tctical.ML	Thu May 31 23:02:16 2007 +0200
     1.2 +++ b/src/Pure/tctical.ML	Thu May 31 23:47:36 2007 +0200
     1.3 @@ -177,10 +177,10 @@
     1.4  fun EVERY1 tacs = EVERY' tacs 1;
     1.5  
     1.6  (* FIRST [tac1,...,tacn]   equals    tac1 ORELSE ... ORELSE tacn   *)
     1.7 -fun FIRST tacs = foldr (op ORELSE) no_tac tacs;
     1.8 +fun FIRST tacs = fold_rev (curry op ORELSE) tacs no_tac;
     1.9  
    1.10  (* FIRST' [tac1,...,tacn] i  equals    tac1 i ORELSE ... ORELSE tacn i   *)
    1.11 -fun FIRST' tacs = foldr (op ORELSE') (K no_tac) tacs;
    1.12 +fun FIRST' tacs = fold_rev (curry op ORELSE') tacs (K no_tac);
    1.13  
    1.14  (*Apply first tactic to 1*)
    1.15  fun FIRST1 tacs = FIRST' tacs 1;
    1.16 @@ -413,7 +413,7 @@
    1.17  (*Common code for METAHYPS and metahyps_thms*)
    1.18  fun metahyps_split_prem prem =
    1.19    let (*find all vars in the hyps -- should find tvars also!*)
    1.20 -      val hyps_vars = foldr add_term_vars [] (Logic.strip_assums_hyp prem)
    1.21 +      val hyps_vars = List.foldr add_term_vars [] (Logic.strip_assums_hyp prem)
    1.22        val insts = map mk_inst hyps_vars
    1.23        (*replace the hyps_vars by Frees*)
    1.24        val prem' = subst_atomic insts prem
    1.25 @@ -453,7 +453,7 @@
    1.26        fun relift st =
    1.27          let val prop = Thm.prop_of st
    1.28              val subgoal_vars = (*Vars introduced in the subgoals*)
    1.29 -                  foldr add_term_vars [] (Logic.strip_imp_prems prop)
    1.30 +                  List.foldr add_term_vars [] (Logic.strip_imp_prems prop)
    1.31              and concl_vars = add_term_vars (Logic.strip_imp_concl prop, [])
    1.32              val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
    1.33              val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st