simplified/unified list fold;
authorwenzelm
Thu May 31 23:47:36 2007 +0200 (2007-05-31 ago)
changeset 2317807ba6b58b3d2
parent 23177 3004310c95b1
child 23179 8db2b22257bd
simplified/unified list fold;
src/Provers/classical.ML
src/Pure/General/seq.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/Proof/reconstruct.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Tools/nbe_eval.ML
src/Pure/codegen.ML
src/Pure/drule.ML
src/Pure/meta_simplifier.ML
src/Pure/net.ML
src/Pure/proofterm.ML
src/Pure/search.ML
src/Pure/tactic.ML
src/Pure/tctical.ML
src/Pure/term.ML
src/Pure/thm.ML
src/Pure/type.ML
src/Pure/unify.ML
     1.1 --- a/src/Provers/classical.ML	Thu May 31 23:02:16 2007 +0200
     1.2 +++ b/src/Provers/classical.ML	Thu May 31 23:47:36 2007 +0200
     1.3 @@ -326,7 +326,7 @@
     1.4  fun tag_brls' _ _ [] = []
     1.5    | tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls;
     1.6  
     1.7 -fun insert_tagged_list kbrls netpr = foldr Tactic.insert_tagged_brl netpr kbrls;
     1.8 +fun insert_tagged_list rls = fold_rev Tactic.insert_tagged_brl rls;
     1.9  
    1.10  (*Insert into netpair that already has nI intr rules and nE elim rules.
    1.11    Count the intr rules double (to account for swapify).  Negate to give the
    1.12 @@ -334,7 +334,7 @@
    1.13  fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules;
    1.14  fun insert' w (nI, nE) = insert_tagged_list o tag_brls' w (~(nI + nE)) o joinrules';
    1.15  
    1.16 -fun delete_tagged_list brls netpr = foldr Tactic.delete_tagged_brl netpr brls;
    1.17 +fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls;
    1.18  fun delete x = delete_tagged_list (joinrules x);
    1.19  fun delete' x = delete_tagged_list (joinrules' x);
    1.20  
     2.1 --- a/src/Pure/General/seq.ML	Thu May 31 23:02:16 2007 +0200
     2.2 +++ b/src/Pure/General/seq.ML	Thu May 31 23:47:36 2007 +0200
     2.3 @@ -202,8 +202,8 @@
     2.4  fun op APPEND (f, g) x =
     2.5    append (f x) (make (fn () => pull (g x)));
     2.6  
     2.7 -fun EVERY fs = foldr THEN succeed fs;
     2.8 -fun FIRST fs = foldr ORELSE fail fs;
     2.9 +fun EVERY fs = fold_rev (curry op THEN) fs succeed;
    2.10 +fun FIRST fs = fold_rev (curry op ORELSE) fs fail;
    2.11  
    2.12  fun TRY f = ORELSE (f, succeed);
    2.13  
     3.1 --- a/src/Pure/Isar/context_rules.ML	Thu May 31 23:02:16 2007 +0200
     3.2 +++ b/src/Pure/Isar/context_rules.ML	Thu May 31 23:47:36 2007 +0200
     3.3 @@ -80,13 +80,13 @@
     3.4  fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) =
     3.5    let val w = (case opt_w of SOME w => w | NONE => Tactic.subgoals_of_brl (b, th)) in
     3.6      make_rules (next - 1) ((w, ((i, b), th)) :: rules)
     3.7 -      (nth_map i (curry insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
     3.8 +      (nth_map i (insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
     3.9    end;
    3.10  
    3.11  fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
    3.12    let
    3.13      fun eq_th (_, (_, th')) = Thm.eq_thm_prop (th, th');
    3.14 -    fun del b netpair = delete_tagged_brl ((b, th), netpair) handle Net.DELETE => netpair;
    3.15 +    fun del b netpair = delete_tagged_brl (b, th) netpair handle Net.DELETE => netpair;
    3.16    in
    3.17      if not (exists eq_th rules) then rs
    3.18      else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
    3.19 @@ -107,7 +107,7 @@
    3.20            k1 = k2 andalso Thm.eq_thm_prop (th1, th2)) (rules1, rules2);
    3.21        val next = ~ (length rules);
    3.22        val netpairs = fold (fn (n, (w, ((i, b), th))) =>
    3.23 -          nth_map i (curry insert_tagged_brl ((w, n), (b, th))))
    3.24 +          nth_map i (insert_tagged_brl ((w, n), (b, th))))
    3.25          (next upto ~1 ~~ rules) empty_netpairs;
    3.26      in make_rules (next - 1) rules netpairs wrappers end
    3.27  );
     4.1 --- a/src/Pure/Isar/locale.ML	Thu May 31 23:02:16 2007 +0200
     4.2 +++ b/src/Pure/Isar/locale.ML	Thu May 31 23:47:36 2007 +0200
     4.3 @@ -664,7 +664,7 @@
     4.4      val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
     4.5  
     4.6      fun inst_parms (i, ps) =
     4.7 -      foldr Term.add_typ_tfrees [] (map_filter snd ps)
     4.8 +      List.foldr Term.add_typ_tfrees [] (map_filter snd ps)
     4.9        |> map_filter (fn (a, S) =>
    4.10            let val T = Envir.norm_type unifier' (TVar ((a, i), S))
    4.11            in if T = TFree (a, S) then NONE else SOME (a, T) end)
    4.12 @@ -1707,7 +1707,7 @@
    4.13      val env = Term.add_term_free_names (body, []);
    4.14      val xs = filter (member (op =) env o #1) parms;
    4.15      val Ts = map #2 xs;
    4.16 -    val extraTs = (Term.term_tfrees body \\ foldr Term.add_typ_tfrees [] Ts)
    4.17 +    val extraTs = (Term.term_tfrees body \\ List.foldr Term.add_typ_tfrees [] Ts)
    4.18        |> Library.sort_wrt #1 |> map TFree;
    4.19      val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
    4.20  
    4.21 @@ -1855,8 +1855,8 @@
    4.22          map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
    4.23      val imports = prep_expr thy raw_imports;
    4.24  
    4.25 -    val extraTs = foldr Term.add_term_tfrees [] exts' \\
    4.26 -      foldr Term.add_typ_tfrees [] (map snd parms);
    4.27 +    val extraTs = List.foldr Term.add_term_tfrees [] exts' \\
    4.28 +      List.foldr Term.add_typ_tfrees [] (map snd parms);
    4.29      val _ = if null extraTs then ()
    4.30        else warning ("Additional type variable(s) in locale specification " ^ quote bname);
    4.31  
     5.1 --- a/src/Pure/Isar/method.ML	Thu May 31 23:02:16 2007 +0200
     5.2 +++ b/src/Pure/Isar/method.ML	Thu May 31 23:47:36 2007 +0200
     5.3 @@ -216,7 +216,8 @@
     5.4  local
     5.5  
     5.6  fun asm_tac ths =
     5.7 -  foldr (op APPEND') (K no_tac) (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths);
     5.8 +  fold_rev (curry op APPEND')
     5.9 +    (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths) (K no_tac);
    5.10  
    5.11  fun cond_rtac cond rule = SUBGOAL (fn (prop, i) =>
    5.12    if cond (Logic.strip_assums_concl prop)
     6.1 --- a/src/Pure/Proof/extraction.ML	Thu May 31 23:02:16 2007 +0200
     6.2 +++ b/src/Pure/Proof/extraction.ML	Thu May 31 23:47:36 2007 +0200
     6.3 @@ -84,7 +84,7 @@
     6.4  
     6.5  fun merge_rules
     6.6    ({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) =
     6.7 -  foldr add_rule {next = next, rs = rs1, net = net} (subtract (op =) rs1 rs2);
     6.8 +  List.foldr add_rule {next = next, rs = rs1, net = net} (subtract (op =) rs1 rs2);
     6.9  
    6.10  fun condrew thy rules procs =
    6.11    let
    6.12 @@ -136,7 +136,7 @@
    6.13    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    6.14    in Abst (a, SOME T, prf_abstract_over t prf) end;
    6.15  
    6.16 -val mkabs = foldr (fn (v, t) => Abs ("x", fastype_of v, abstract_over (v, t)));
    6.17 +val mkabs = List.foldr (fn (v, t) => Abs ("x", fastype_of v, abstract_over (v, t)));
    6.18  
    6.19  fun strip_abs 0 t = t
    6.20    | strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t
    6.21 @@ -145,7 +145,7 @@
    6.22  fun prf_subst_TVars tye =
    6.23    map_proof_terms (subst_TVars tye) (typ_subst_TVars tye);
    6.24  
    6.25 -fun relevant_vars types prop = foldr (fn
    6.26 +fun relevant_vars types prop = List.foldr (fn
    6.27        (Var ((a, i), T), vs) => (case strip_type T of
    6.28          (_, Type (s, _)) => if member (op =) types s then a :: vs else vs
    6.29        | _ => vs)
    6.30 @@ -237,7 +237,7 @@
    6.31      defs, expand, prep} = ExtractionData.get thy;
    6.32    in
    6.33      ExtractionData.put
    6.34 -      {realizes_eqns = foldr add_rule realizes_eqns (map (prep_eq thy) eqns),
    6.35 +      {realizes_eqns = List.foldr add_rule realizes_eqns (map (prep_eq thy) eqns),
    6.36         typeof_eqns = typeof_eqns, types = types, realizers = realizers,
    6.37         defs = defs, expand = expand, prep = prep} thy
    6.38    end
    6.39 @@ -255,7 +255,7 @@
    6.40    in
    6.41      ExtractionData.put
    6.42        {realizes_eqns = realizes_eqns, realizers = realizers,
    6.43 -       typeof_eqns = foldr add_rule typeof_eqns eqns',
    6.44 +       typeof_eqns = List.foldr add_rule typeof_eqns eqns',
    6.45         types = types, defs = defs, expand = expand, prep = prep} thy
    6.46    end
    6.47  
    6.48 @@ -324,7 +324,7 @@
    6.49          (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
    6.50            (Const ("realizes", T --> propT --> propT) $
    6.51              (if T = nullT then t else list_comb (t, vars')) $ prop);
    6.52 -      val r = foldr forall_intr r' (map (get_var_type r') vars);
    6.53 +      val r = List.foldr forall_intr r' (map (get_var_type r') vars);
    6.54        val prf = Reconstruct.reconstruct_proof thy' r (rd s2);
    6.55      in (name, (vs, (t, prf))) end
    6.56    end;
    6.57 @@ -474,7 +474,7 @@
    6.58              end
    6.59            else (vs', tye)
    6.60  
    6.61 -      in foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
    6.62 +      in List.foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
    6.63  
    6.64      fun find (vs: string list) = Option.map snd o find_first (curry (gen_eq_set (op =)) vs o fst);
    6.65      fun find' s = map snd o List.filter (equal s o fst)
    6.66 @@ -569,7 +569,7 @@
    6.67                      val (defs'', corr_prf) =
    6.68                        corr (d + 1) defs' vs' [] [] [] prf' prf' NONE;
    6.69                      val corr_prop = Reconstruct.prop_of corr_prf;
    6.70 -                    val corr_prf' = foldr forall_intr_prf
    6.71 +                    val corr_prf' = List.foldr forall_intr_prf
    6.72                        (proof_combt
    6.73                           (PThm (corr_name name vs', corr_prf, corr_prop,
    6.74                               SOME (map TVar (term_tvars corr_prop))), vfs_of corr_prop))
    6.75 @@ -678,7 +678,7 @@
    6.76                             PAxm (cname ^ "_def", eqn,
    6.77                               SOME (map TVar (term_tvars eqn))))) %% corr_prf;
    6.78                      val corr_prop = Reconstruct.prop_of corr_prf';
    6.79 -                    val corr_prf'' = foldr forall_intr_prf
    6.80 +                    val corr_prf'' = List.foldr forall_intr_prf
    6.81                        (proof_combt
    6.82                          (PThm (corr_name s vs', corr_prf', corr_prop,
    6.83                            SOME (map TVar (term_tvars corr_prop))),  vfs_of corr_prop))
     7.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Thu May 31 23:02:16 2007 +0200
     7.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Thu May 31 23:47:36 2007 +0200
     7.3 @@ -231,7 +231,7 @@
     7.4                val tvars = term_tvars prop;
     7.5                val (_, rhs) = Logic.dest_equals prop;
     7.6                val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
     7.7 -                (foldr (fn p => Abs ("", dummyT, abstract_over p)) rhs vs),
     7.8 +                (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
     7.9                  map the ts);
    7.10              in
    7.11                change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'
     8.1 --- a/src/Pure/Proof/reconstruct.ML	Thu May 31 23:02:16 2007 +0200
     8.2 +++ b/src/Pure/Proof/reconstruct.ML	Thu May 31 23:47:36 2007 +0200
     8.3 @@ -26,19 +26,19 @@
     8.4  fun vars_of t = rev (fold_aterms
     8.5    (fn v as Var _ => insert (op =) v | _ => I) t []);
     8.6  
     8.7 -fun forall_intr (t, prop) =
     8.8 +fun forall_intr t prop =
     8.9    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    8.10    in all T $ Abs (a, T, abstract_over (t, prop)) end;
    8.11  
    8.12 -fun forall_intr_vfs prop = foldr forall_intr prop
    8.13 -  (vars_of prop @ sort Term.term_ord (term_frees prop));
    8.14 +fun forall_intr_vfs prop = fold_rev forall_intr
    8.15 +  (vars_of prop @ sort Term.term_ord (term_frees prop)) prop;
    8.16  
    8.17 -fun forall_intr_prf (t, prf) =
    8.18 +fun forall_intr_prf t prf =
    8.19    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    8.20    in Abst (a, SOME T, prf_abstract_over t prf) end;
    8.21  
    8.22 -fun forall_intr_vfs_prf prop prf = foldr forall_intr_prf prf
    8.23 -  (vars_of prop @ sort Term.term_ord (term_frees prop));
    8.24 +fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_prf
    8.25 +  (vars_of prop @ sort Term.term_ord (term_frees prop)) prf;
    8.26  
    8.27  fun merge_envs (Envir.Envir {asol=asol1, iTs=iTs1, maxidx=maxidx1})
    8.28    (Envir.Envir {asol=asol2, iTs=iTs2, maxidx=maxidx2}) =
    8.29 @@ -49,7 +49,7 @@
    8.30  
    8.31  (**** generate constraints for proof term ****)
    8.32  
    8.33 -fun mk_var env Ts T = 
    8.34 +fun mk_var env Ts T =
    8.35    let val (env', v) = Envir.genvar "a" (env, rev Ts ---> T)
    8.36    in (env', list_comb (v, map Bound (length Ts - 1 downto 0))) end;
    8.37  
    8.38 @@ -74,7 +74,7 @@
    8.39  fun infer_type thy (env as Envir.Envir {maxidx, asol, iTs}) Ts vTs
    8.40        (t as Const (s, T)) = if T = dummyT then (case Sign.const_type thy s of
    8.41            NONE => error ("reconstruct_proof: No such constant: " ^ quote s)
    8.42 -        | SOME T => 
    8.43 +        | SOME T =>
    8.44              let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T)
    8.45              in (Const (s, T'), T', vTs,
    8.46                Envir.Envir {maxidx = maxidx + 1, asol = asol, iTs = iTs})
    8.47 @@ -156,7 +156,7 @@
    8.48  
    8.49      fun head_norm (prop, prf, cnstrts, env, vTs) =
    8.50        (Envir.head_norm env prop, prf, cnstrts, env, vTs);
    8.51 - 
    8.52 +
    8.53      fun mk_cnstrts env _ Hs vTs (PBound i) = (List.nth (Hs, i), PBound i, [], env, vTs)
    8.54        | mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) =
    8.55            let
    8.56 @@ -338,10 +338,10 @@
    8.57  
    8.58  fun expand_proof thy thms prf =
    8.59    let
    8.60 -    fun expand maxidx prfs (AbsP (s, t, prf)) = 
    8.61 +    fun expand maxidx prfs (AbsP (s, t, prf)) =
    8.62            let val (maxidx', prfs', prf') = expand maxidx prfs prf
    8.63            in (maxidx', prfs', AbsP (s, t, prf')) end
    8.64 -      | expand maxidx prfs (Abst (s, T, prf)) = 
    8.65 +      | expand maxidx prfs (Abst (s, T, prf)) =
    8.66            let val (maxidx', prfs', prf') = expand maxidx prfs prf
    8.67            in (maxidx', prfs', Abst (s, T, prf')) end
    8.68        | expand maxidx prfs (prf1 %% prf2) =
     9.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu May 31 23:02:16 2007 +0200
     9.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu May 31 23:47:36 2007 +0200
     9.3 @@ -594,7 +594,7 @@
     9.4                                      x::_::_ => SOME x  (* String.find? *)
     9.5                                    | _ => NONE
     9.6          fun subthys_of_thy s =
     9.7 -            foldl  (fn (NONE,xs) => xs | (SOME x,xs) => insert op= x xs) []
     9.8 +            List.foldl  (fn (NONE,xs) => xs | (SOME x,xs) => insert op= x xs) []
     9.9                     (map thy_prefix (thms_of_thy s))
    9.10          fun subthms_of_thy thy =
    9.11              (case thy_prefix thy of
    10.1 --- a/src/Pure/Tools/nbe_eval.ML	Thu May 31 23:02:16 2007 +0200
    10.2 +++ b/src/Pure/Tools/nbe_eval.ML	Thu May 31 23:47:36 2007 +0200
    10.3 @@ -56,7 +56,7 @@
    10.4    | string_of_nterm(AbsN(n,t)) =
    10.5        "(Abs " ^ string_of_int n ^ " " ^ string_of_nterm t ^ ")";
    10.6  
    10.7 -fun apps t args = foldr (fn (y,x) => A(x,y)) t args;
    10.8 +fun apps t args = fold_rev (fn y => fn x => A(x,y)) args t;
    10.9  
   10.10  (* ------------------------------ The semantical universe --------------------- *)
   10.11  
    11.1 --- a/src/Pure/codegen.ML	Thu May 31 23:02:16 2007 +0200
    11.2 +++ b/src/Pure/codegen.ML	Thu May 31 23:47:36 2007 +0200
    11.3 @@ -359,7 +359,7 @@
    11.4  fun mk_parser (a, p) = (if a = "" then Scan.succeed "" else Args.$$$ a) |-- p;
    11.5  
    11.6  val code_attr =
    11.7 -  Attrib.syntax (Scan.peek (fn context => foldr op || Scan.fail (map mk_parser
    11.8 +  Attrib.syntax (Scan.peek (fn context => List.foldr op || Scan.fail (map mk_parser
    11.9      (#attrs (CodegenData.get (Context.theory_of context))))));
   11.10  
   11.11  val _ = Context.add_setup
   11.12 @@ -542,7 +542,7 @@
   11.13  
   11.14  fun rename_terms ts =
   11.15    let
   11.16 -    val names = foldr add_term_names
   11.17 +    val names = List.foldr add_term_names
   11.18        (map (fst o fst) (rev (fold Term.add_vars ts []))) ts;
   11.19      val reserved = filter ML_Syntax.is_reserved names;
   11.20      val (illegal, alt_names) = split_list (map_filter (fn s =>
   11.21 @@ -684,7 +684,7 @@
   11.22      val (Ts, _) = strip_type (fastype_of t);
   11.23      val j = i - length ts
   11.24    in
   11.25 -    foldr (fn (T, t) => Abs ("x", T, t))
   11.26 +    List.foldr (fn (T, t) => Abs ("x", T, t))
   11.27        (list_comb (t, ts @ map Bound (j-1 downto 0))) (Library.take (j, Ts))
   11.28    end;
   11.29  
   11.30 @@ -862,15 +862,15 @@
   11.31      if module = "" then
   11.32        let
   11.33          val modules = distinct (op =) (map (#2 o snd) code);
   11.34 -        val mod_gr = foldr (uncurry Graph.add_edge_acyclic)
   11.35 -          (foldr (uncurry (Graph.new_node o rpair ())) Graph.empty modules)
   11.36 +        val mod_gr = fold_rev Graph.add_edge_acyclic
   11.37            (maps (fn (s, (_, module, _)) => map (pair module)
   11.38              (filter_out (equal module) (map (#2 o Graph.get_node gr)
   11.39 -              (Graph.imm_succs gr s)))) code);
   11.40 +              (Graph.imm_succs gr s)))) code)
   11.41 +          (fold_rev (Graph.new_node o rpair ()) modules Graph.empty);
   11.42          val modules' =
   11.43            rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs))
   11.44        in
   11.45 -        foldl (fn ((_, (_, module, s)), ms) => add_to_module module s ms)
   11.46 +        List.foldl (fn ((_, (_, module, s)), ms) => add_to_module module s ms)
   11.47            (map (rpair "") modules') code
   11.48        end handle Graph.CYCLES (cs :: _) =>
   11.49          error ("Cyclic dependency of modules:\n" ^ commas cs ^
   11.50 @@ -887,7 +887,7 @@
   11.51      val graphs = get_modules thy;
   11.52      val defs = mk_deftab thy;
   11.53      val gr = new_node ("<Top>", (NONE, module, ""))
   11.54 -      (foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) =>
   11.55 +      (List.foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) =>
   11.56          (Graph.merge (fn ((_, module, _), (_, module', _)) =>
   11.57             module = module') (gr, gr'),
   11.58           (merge_nametabs (tab1, tab1'), merge_nametabs (tab2, tab2')))) emptygr
    12.1 --- a/src/Pure/drule.ML	Thu May 31 23:02:16 2007 +0200
    12.2 +++ b/src/Pure/drule.ML	Thu May 31 23:47:36 2007 +0200
    12.3 @@ -401,7 +401,7 @@
    12.4   let val fth = Thm.freezeT th
    12.5       val {prop, tpairs, thy, ...} = rep_thm fth
    12.6   in
    12.7 -   case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
    12.8 +   case List.foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
    12.9         [] => (fth, fn i => fn x => x)   (*No vars: nothing to do!*)
   12.10       | vars =>
   12.11           let fun newName (Var(ix,_)) = (ix, gensym (string_of_indexname ix))
   12.12 @@ -423,13 +423,13 @@
   12.13   let val fth = Thm.freezeT th
   12.14       val {prop, tpairs, thy, ...} = rep_thm fth
   12.15   in
   12.16 -   case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
   12.17 +   case List.foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
   12.18         [] => (fth, fn x => x)
   12.19       | vars =>
   12.20           let fun newName (Var(ix,_), (pairs,used)) =
   12.21                     let val v = Name.variant used (string_of_indexname ix)
   12.22                     in  ((ix,v)::pairs, v::used)  end;
   12.23 -             val (alist, _) = foldr newName ([], Library.foldr add_term_names
   12.24 +             val (alist, _) = List.foldr newName ([], Library.foldr add_term_names
   12.25                 (prop :: Thm.terms_of_tpairs tpairs, [])) vars
   12.26               fun mk_inst (Var(v,T)) =
   12.27                   (cterm_of thy (Var(v,T)),
   12.28 @@ -810,7 +810,7 @@
   12.29  in
   12.30  fun cterm_instantiate [] th = th
   12.31    | cterm_instantiate ctpairs0 th =
   12.32 -  let val (thy,tye,_) = foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0
   12.33 +  let val (thy,tye,_) = List.foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0
   12.34        fun instT(ct,cu) =
   12.35          let val inst = cterm_of thy o Term.map_types (Envir.norm_type tye) o term_of
   12.36          in (inst ct, inst cu) end
    13.1 --- a/src/Pure/meta_simplifier.ML	Thu May 31 23:02:16 2007 +0200
    13.2 +++ b/src/Pure/meta_simplifier.ML	Thu May 31 23:47:36 2007 +0200
    13.3 @@ -1107,7 +1107,7 @@
    13.4      and add_rrules (rrss, asms) ss =
    13.5        (fold o fold) insert_rrule rrss ss |> add_prems (map_filter I asms)
    13.6  
    13.7 -    and disch r (prem, eq) =
    13.8 +    and disch r prem eq =
    13.9        let
   13.10          val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
   13.11          val eq' = implies_elim (Thm.instantiate
   13.12 @@ -1131,11 +1131,11 @@
   13.13              val ss' = add_rrules (rev rrss, rev asms) ss;
   13.14              val concl' =
   13.15                Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq));
   13.16 -            val dprem = Option.map (curry (disch false) prem)
   13.17 +            val dprem = Option.map (disch false prem)
   13.18            in case rewritec (prover, thy, maxidx) ss' concl' of
   13.19                NONE => rebuild prems concl' rrss asms ss (dprem eq)
   13.20 -            | SOME (eq', _) => transitive2 (Library.foldl (disch false o swap)
   13.21 -                  (the (transitive3 (dprem eq) eq'), prems))
   13.22 +            | SOME (eq', _) => transitive2 (fold (disch false)
   13.23 +                  prems (the (transitive3 (dprem eq) eq')))
   13.24                  (mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ss)
   13.25            end
   13.26  
   13.27 @@ -1149,7 +1149,7 @@
   13.28  
   13.29      and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k =
   13.30          transitive1 (Library.foldl (fn (eq2, (eq1, prem)) => transitive1 eq1
   13.31 -            (Option.map (curry (disch false) prem) eq2)) (NONE, eqns ~~ prems'))
   13.32 +            (Option.map (disch false prem) eq2)) (NONE, eqns ~~ prems'))
   13.33            (if changed > 0 then
   13.34               mut_impc (rev prems') concl (rev rrss') (rev asms')
   13.35                 [] [] [] [] ss ~1 changed
   13.36 @@ -1171,9 +1171,10 @@
   13.37                  find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn)));
   13.38                val (rrs', asm') = rules_of_prem ss prem'
   13.39              in mut_impc prems concl rrss asms (prem' :: prems')
   13.40 -              (rrs' :: rrss') (asm' :: asms') (SOME (foldr (disch true)
   13.41 +              (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
   13.42 +                (Library.take (i, prems))
   13.43                  (Drule.imp_cong_rule eqn (reflexive (Drule.list_implies
   13.44 -                  (Library.drop (i, prems), concl)))) (Library.take (i, prems))) :: eqns)
   13.45 +                  (Library.drop (i, prems), concl))))) :: eqns)
   13.46                    ss (length prems') ~1
   13.47              end
   13.48  
   13.49 @@ -1189,7 +1190,7 @@
   13.50                 NONE => NONE
   13.51               | SOME thm1' => SOME (Drule.imp_cong_rule thm1' (reflexive conc)))
   13.52           | SOME thm2 =>
   13.53 -           let val thm2' = disch false (prem1, thm2)
   13.54 +           let val thm2' = disch false prem1 thm2
   13.55             in (case thm1 of
   13.56                 NONE => SOME thm2'
   13.57               | SOME thm1' =>
    14.1 --- a/src/Pure/net.ML	Thu May 31 23:02:16 2007 +0200
    14.2 +++ b/src/Pure/net.ML	Thu May 31 23:47:36 2007 +0200
    14.3 @@ -158,9 +158,9 @@
    14.4  
    14.5  
    14.6  (*Skipping a term in a net.  Recursively skip 2 levels if a combination*)
    14.7 -fun net_skip (Leaf _, nets) = nets
    14.8 -  | net_skip (Net{comb,var,atoms}, nets) =
    14.9 -      foldr net_skip (Symtab.fold (cons o #2) atoms (var::nets)) (net_skip (comb,[]));
   14.10 +fun net_skip (Leaf _) nets = nets
   14.11 +  | net_skip (Net{comb,var,atoms}) nets =
   14.12 +      fold_rev net_skip (net_skip comb []) (Symtab.fold (cons o #2) atoms (var::nets));
   14.13  
   14.14  
   14.15  (** Matching and Unification **)
   14.16 @@ -175,11 +175,11 @@
   14.17    Abs or Var in object: if "unif", regarded as wildcard,
   14.18                                     else matches only a variable in net.
   14.19  *)
   14.20 -fun matching unif t (net,nets) =
   14.21 +fun matching unif t net nets =
   14.22    let fun rands _ (Leaf _, nets) = nets
   14.23          | rands t (Net{comb,atoms,...}, nets) =
   14.24              case t of
   14.25 -                f$t => foldr (matching unif t) nets (rands f (comb,[]))
   14.26 +                f$t => fold_rev (matching unif t) (rands f (comb,[])) nets
   14.27                | Const(c,_) => look1 (atoms, c) nets
   14.28                | Free(c,_)  => look1 (atoms, c) nets
   14.29                | Bound i    => look1 (atoms, Name.bound i) nets
   14.30 @@ -189,11 +189,11 @@
   14.31           Leaf _ => nets
   14.32         | Net{var,...} =>
   14.33               case head_of t of
   14.34 -                 Var _ => if unif then net_skip (net,nets)
   14.35 +                 Var _ => if unif then net_skip net nets
   14.36                            else var::nets           (*only matches Var in net*)
   14.37    (*If "unif" then a var instantiation in the abstraction could allow
   14.38      an eta-reduction, so regard the abstraction as a wildcard.*)
   14.39 -               | Abs _ => if unif then net_skip (net,nets)
   14.40 +               | Abs _ => if unif then net_skip net nets
   14.41                            else var::nets           (*only a Var can match*)
   14.42                 | _ => rands t (net, var::nets)  (*var could match also*)
   14.43    end;
   14.44 @@ -202,11 +202,11 @@
   14.45  
   14.46  (*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*)
   14.47  fun match_term net t =
   14.48 -    extract_leaves (matching false t (net,[]));
   14.49 +    extract_leaves (matching false t net []);
   14.50  
   14.51  (*return items whose key could unify with t*)
   14.52  fun unify_term net t =
   14.53 -    extract_leaves (matching true t (net,[]));
   14.54 +    extract_leaves (matching true t net []);
   14.55  
   14.56  
   14.57  (** operations on nets **)
    15.1 --- a/src/Pure/proofterm.ML	Thu May 31 23:02:16 2007 +0200
    15.2 +++ b/src/Pure/proofterm.ML	Thu May 31 23:47:36 2007 +0200
    15.3 @@ -250,7 +250,7 @@
    15.4        (PThm (_, prf', _, _), _) => prf'
    15.5      | _ => prf);
    15.6  
    15.7 -val mk_Abst = foldr (fn ((s, T:typ), prf) => Abst (s, NONE, prf));
    15.8 +val mk_Abst = fold_rev (fn (s, T:typ) => fn prf => Abst (s, NONE, prf));
    15.9  fun mk_AbsP (i, prf) = funpow i (fn prf => AbsP ("H", NONE, prf)) prf;
   15.10  
   15.11  fun apsome f NONE = raise SAME
   15.12 @@ -621,7 +621,7 @@
   15.13    let
   15.14      val used = it_term_types add_typ_tfree_names (t, [])
   15.15      and tvars = map #1 (it_term_types add_typ_tvars (t, []));
   15.16 -    val (alist, _) = foldr new_name ([], used) tvars;
   15.17 +    val (alist, _) = List.foldr new_name ([], used) tvars;
   15.18    in
   15.19      (case alist of
   15.20        [] => prf (*nothing to do!*)
   15.21 @@ -643,9 +643,9 @@
   15.22      val j = length Bs;
   15.23    in
   15.24      mk_AbsP (j+1, proof_combP (prf, map PBound
   15.25 -      (j downto 1) @ [mk_Abst (mk_AbsP (i,
   15.26 +      (j downto 1) @ [mk_Abst params (mk_AbsP (i,
   15.27          proof_combP (proof_combt (PBound i, map Bound ((length params - 1) downto 0)),
   15.28 -          map PBound (((i-m-1) downto 0) @ ((i-1) downto (i-m)))))) params]))
   15.29 +          map PBound (((i-m-1) downto 0) @ ((i-1) downto (i-m))))))]))
   15.30    end;
   15.31  
   15.32  
   15.33 @@ -700,7 +700,7 @@
   15.34      val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop);
   15.35      val k = length ps;
   15.36  
   15.37 -    fun mk_app (b, (i, j, prf)) =
   15.38 +    fun mk_app b (i, j, prf) =
   15.39            if b then (i-1, j, prf %% PBound i) else (i, j-1, prf %> Bound j);
   15.40  
   15.41      fun lift Us bs i j (Const ("==>", _) $ A $ B) =
   15.42 @@ -708,7 +708,7 @@
   15.43        | lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) =
   15.44              Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t)
   15.45        | lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf,
   15.46 -            map (fn k => (#3 (foldr mk_app (i-1, j-1, PBound k) bs)))
   15.47 +            map (fn k => (#3 (fold_rev mk_app bs (i-1, j-1, PBound k))))
   15.48                (i + k - 1 downto i));
   15.49    in
   15.50      mk_AbsP (k, lift [] [] 0 0 Bi)
   15.51 @@ -1200,7 +1200,7 @@
   15.52        map SOME (sort Term.term_ord (term_frees prop));
   15.53      val opt_prf = if ! proofs = 2 then
   15.54          #4 (shrink_proof thy [] 0 (rewrite_prf fst (ProofData.get thy)
   15.55 -          (foldr (uncurry implies_intr_proof) prf hyps)))
   15.56 +          (fold_rev implies_intr_proof hyps prf)))
   15.57        else MinProof (mk_min_proof prf ([], [], []));
   15.58      val head = (case strip_combt (fst (strip_combP prf)) of
   15.59          (PThm (old_name, prf', prop', NONE), args') =>
    16.1 --- a/src/Pure/search.ML	Thu May 31 23:02:16 2007 +0200
    16.2 +++ b/src/Pure/search.ML	Thu May 31 23:47:36 2007 +0200
    16.3 @@ -1,6 +1,6 @@
    16.4 -(*  Title: 	Pure/search.ML
    16.5 +(*  Title:      Pure/search.ML
    16.6      ID:         $Id$
    16.7 -    Author: 	Lawrence C Paulson and Norbert Voelker
    16.8 +    Author:     Lawrence C Paulson and Norbert Voelker
    16.9  
   16.10  Search tacticals.
   16.11  *)
   16.12 @@ -9,33 +9,33 @@
   16.13  
   16.14  signature SEARCH =
   16.15    sig
   16.16 -  val DEEPEN  	        : int*int -> (int->int->tactic) -> int -> int -> tactic
   16.17 +  val DEEPEN            : int*int -> (int->int->tactic) -> int -> int -> tactic
   16.18  
   16.19 -  val THEN_MAYBE	: tactic * tactic -> tactic
   16.20 -  val THEN_MAYBE'	: ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
   16.21 +  val THEN_MAYBE        : tactic * tactic -> tactic
   16.22 +  val THEN_MAYBE'       : ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
   16.23  
   16.24 -  val trace_DEPTH_FIRST	: bool ref
   16.25 -  val DEPTH_FIRST	: (thm -> bool) -> tactic -> tactic
   16.26 -  val DEPTH_SOLVE	: tactic -> tactic
   16.27 -  val DEPTH_SOLVE_1	: tactic -> tactic
   16.28 -  val ITER_DEEPEN	: (thm->bool) -> (int->tactic) -> tactic
   16.29 -  val THEN_ITER_DEEPEN	: tactic -> (thm->bool) -> (int->tactic) -> tactic
   16.30 +  val trace_DEPTH_FIRST : bool ref
   16.31 +  val DEPTH_FIRST       : (thm -> bool) -> tactic -> tactic
   16.32 +  val DEPTH_SOLVE       : tactic -> tactic
   16.33 +  val DEPTH_SOLVE_1     : tactic -> tactic
   16.34 +  val ITER_DEEPEN       : (thm->bool) -> (int->tactic) -> tactic
   16.35 +  val THEN_ITER_DEEPEN  : tactic -> (thm->bool) -> (int->tactic) -> tactic
   16.36    val iter_deepen_limit : int ref
   16.37  
   16.38 -  val has_fewer_prems	: int -> thm -> bool   
   16.39 -  val IF_UNSOLVED	: tactic -> tactic
   16.40 -  val SOLVE		: tactic -> tactic
   16.41 +  val has_fewer_prems   : int -> thm -> bool
   16.42 +  val IF_UNSOLVED       : tactic -> tactic
   16.43 +  val SOLVE             : tactic -> tactic
   16.44    val DETERM_UNTIL_SOLVED: tactic -> tactic
   16.45 -  val trace_BEST_FIRST	: bool ref
   16.46 -  val BEST_FIRST	: (thm -> bool) * (thm -> int) -> tactic -> tactic
   16.47 -  val THEN_BEST_FIRST	: tactic -> (thm->bool) * (thm->int) -> tactic
   16.48 -			  -> tactic
   16.49 -  val trace_ASTAR	: bool ref
   16.50 -  val ASTAR	        : (thm -> bool) * (int->thm->int) -> tactic -> tactic
   16.51 -  val THEN_ASTAR	: tactic -> (thm->bool) * (int->thm->int) -> tactic
   16.52 -			  -> tactic
   16.53 -  val BREADTH_FIRST	: (thm -> bool) -> tactic -> tactic
   16.54 -  val QUIET_BREADTH_FIRST	: (thm -> bool) -> tactic -> tactic
   16.55 +  val trace_BEST_FIRST  : bool ref
   16.56 +  val BEST_FIRST        : (thm -> bool) * (thm -> int) -> tactic -> tactic
   16.57 +  val THEN_BEST_FIRST   : tactic -> (thm->bool) * (thm->int) -> tactic
   16.58 +                          -> tactic
   16.59 +  val trace_ASTAR       : bool ref
   16.60 +  val ASTAR             : (thm -> bool) * (int->thm->int) -> tactic -> tactic
   16.61 +  val THEN_ASTAR        : tactic -> (thm->bool) * (int->thm->int) -> tactic
   16.62 +                          -> tactic
   16.63 +  val BREADTH_FIRST     : (thm -> bool) -> tactic -> tactic
   16.64 +  val QUIET_BREADTH_FIRST       : (thm -> bool) -> tactic -> tactic
   16.65    end;
   16.66  
   16.67  
   16.68 @@ -48,7 +48,7 @@
   16.69        (Term.term_ord o Library.pairself (#prop o Thm.rep_thm)));
   16.70  
   16.71  
   16.72 -structure Search : SEARCH = 
   16.73 +structure Search : SEARCH =
   16.74  struct
   16.75  
   16.76  (**** Depth-first search ****)
   16.77 @@ -57,17 +57,17 @@
   16.78  
   16.79  (*Searches until "satp" reports proof tree as satisfied.
   16.80    Suppresses duplicate solutions to minimize search space.*)
   16.81 -fun DEPTH_FIRST satp tac = 
   16.82 +fun DEPTH_FIRST satp tac =
   16.83   let val tac = tracify trace_DEPTH_FIRST tac
   16.84       fun depth used [] = NONE
   16.85         | depth used (q::qs) =
   16.86 -	  case Seq.pull q of
   16.87 -	      NONE         => depth used qs
   16.88 -	    | SOME(st,stq) => 
   16.89 -		if satp st andalso not (member Thm.eq_thm used st)
   16.90 -		then SOME(st, Seq.make
   16.91 -			         (fn()=> depth (st::used) (stq::qs)))
   16.92 -		else depth used (tac st :: stq :: qs)
   16.93 +          case Seq.pull q of
   16.94 +              NONE         => depth used qs
   16.95 +            | SOME(st,stq) =>
   16.96 +                if satp st andalso not (member Thm.eq_thm used st)
   16.97 +                then SOME(st, Seq.make
   16.98 +                                 (fn()=> depth (st::used) (stq::qs)))
   16.99 +                else depth used (tac st :: stq :: qs)
  16.100    in  traced_tac (fn st => depth [] [Seq.single st])  end;
  16.101  
  16.102  
  16.103 @@ -86,7 +86,7 @@
  16.104  
  16.105  (*Execute tac1, but only execute tac2 if there are at least as many subgoals
  16.106    as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
  16.107 -fun (tac1 THEN_MAYBE tac2) st = 
  16.108 +fun (tac1 THEN_MAYBE tac2) st =
  16.109      (tac1  THEN  COND (has_fewer_prems (nprems_of st)) all_tac tac2)  st;
  16.110  
  16.111  fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x;
  16.112 @@ -95,7 +95,7 @@
  16.113    If no subgoals then it must fail! *)
  16.114  fun DEPTH_SOLVE_1 tac st = st |>
  16.115      (case nprems_of st of
  16.116 -	0 => no_tac
  16.117 +        0 => no_tac
  16.118        | n => DEPTH_FIRST (has_fewer_prems n) tac);
  16.119  
  16.120  (*Uses depth-first search to solve ALL subgoals*)
  16.121 @@ -114,21 +114,21 @@
  16.122    may perform >1 inference*)
  16.123  
  16.124  (*Pruning of rigid ancestor to prevent backtracking*)
  16.125 -fun prune (new as (k', np':int, rgd', stq), qs) = 
  16.126 +fun prune (new as (k', np':int, rgd', stq), qs) =
  16.127      let fun prune_aux (qs, []) = new::qs
  16.128            | prune_aux (qs, (k,np,rgd,q)::rqs) =
  16.129 -	      if np'+1 = np andalso rgd then
  16.130 -		  (if !trace_DEPTH_FIRST then
  16.131 -		       tracing ("Pruning " ^ 
  16.132 -				string_of_int (1+length rqs) ^ " levels")
  16.133 -		   else ();
  16.134 -		   (*Use OLD k: zero-cost solution; see Stickel, p 365*)
  16.135 -		   (k, np', rgd', stq) :: qs)
  16.136 -	      else prune_aux ((k,np,rgd,q)::qs, rqs)
  16.137 +              if np'+1 = np andalso rgd then
  16.138 +                  (if !trace_DEPTH_FIRST then
  16.139 +                       tracing ("Pruning " ^
  16.140 +                                string_of_int (1+length rqs) ^ " levels")
  16.141 +                   else ();
  16.142 +                   (*Use OLD k: zero-cost solution; see Stickel, p 365*)
  16.143 +                   (k, np', rgd', stq) :: qs)
  16.144 +              else prune_aux ((k,np,rgd,q)::qs, rqs)
  16.145          fun take ([], rqs) = ([], rqs)
  16.146 -	  | take (arg as ((k,np,rgd,stq)::qs, rqs)) = 
  16.147 -	        if np' < np then take (qs, (k,np,rgd,stq)::rqs)
  16.148 -		            else arg
  16.149 +          | take (arg as ((k,np,rgd,stq)::qs, rqs)) =
  16.150 +                if np' < np then take (qs, (k,np,rgd,stq)::rqs)
  16.151 +                            else arg
  16.152      in  prune_aux (take (qs, []))  end;
  16.153  
  16.154  
  16.155 @@ -140,49 +140,49 @@
  16.156    The solution sequence is redundant: the cutoff heuristic makes it impossible
  16.157    to suppress solutions arising from earlier searches, as the accumulated cost
  16.158    (k) can be wrong.*)
  16.159 -fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st => 
  16.160 +fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st =>
  16.161   let val countr = ref 0
  16.162       and tf = tracify trace_DEPTH_FIRST (tac1 1)
  16.163       and qs0 = tac0 st
  16.164       (*bnd = depth bound; inc = estimate of increment required next*)
  16.165 -     fun depth (bnd,inc) [] = 
  16.166 +     fun depth (bnd,inc) [] =
  16.167            if bnd > !iter_deepen_limit then
  16.168 -	     (tracing (string_of_int (!countr) ^ 
  16.169 -		       " inferences so far.  Giving up at " ^ string_of_int bnd);
  16.170 -	      NONE)
  16.171 +             (tracing (string_of_int (!countr) ^
  16.172 +                       " inferences so far.  Giving up at " ^ string_of_int bnd);
  16.173 +              NONE)
  16.174            else
  16.175 -	     (tracing (string_of_int (!countr) ^ 
  16.176 -		       " inferences so far.  Searching to depth " ^ 
  16.177 -		       string_of_int bnd);
  16.178 -	      (*larger increments make it run slower for the hard problems*)
  16.179 -	      depth (bnd+inc, 10)) [(0, 1, false, qs0)]
  16.180 +             (tracing (string_of_int (!countr) ^
  16.181 +                       " inferences so far.  Searching to depth " ^
  16.182 +                       string_of_int bnd);
  16.183 +              (*larger increments make it run slower for the hard problems*)
  16.184 +              depth (bnd+inc, 10)) [(0, 1, false, qs0)]
  16.185         | depth (bnd,inc) ((k,np,rgd,q)::qs) =
  16.186 -	  if k>=bnd then depth (bnd,inc) qs
  16.187 +          if k>=bnd then depth (bnd,inc) qs
  16.188            else
  16.189 -	  case (countr := !countr+1;
  16.190 -		if !trace_DEPTH_FIRST then
  16.191 -		    tracing (string_of_int np ^ implode (map (fn _ => "*") qs))
  16.192 -		else ();
  16.193 -		Seq.pull q) of
  16.194 -	     NONE         => depth (bnd,inc) qs
  16.195 -	   | SOME(st,stq) => 
  16.196 -	       if satp st	(*solution!*)
  16.197 -	       then SOME(st, Seq.make
  16.198 -			 (fn()=> depth (bnd,inc) ((k,np,rgd,stq)::qs)))
  16.199 +          case (countr := !countr+1;
  16.200 +                if !trace_DEPTH_FIRST then
  16.201 +                    tracing (string_of_int np ^ implode (map (fn _ => "*") qs))
  16.202 +                else ();
  16.203 +                Seq.pull q) of
  16.204 +             NONE         => depth (bnd,inc) qs
  16.205 +           | SOME(st,stq) =>
  16.206 +               if satp st       (*solution!*)
  16.207 +               then SOME(st, Seq.make
  16.208 +                         (fn()=> depth (bnd,inc) ((k,np,rgd,stq)::qs)))
  16.209  
  16.210 -	       else 
  16.211 +               else
  16.212                 let val np' = nprems_of st
  16.213 -		     (*rgd' calculation assumes tactic operates on subgoal 1*)
  16.214 +                     (*rgd' calculation assumes tactic operates on subgoal 1*)
  16.215                     val rgd' = not (has_vars (hd (prems_of st)))
  16.216                     val k' = k+np'-np+1  (*difference in # of subgoals, +1*)
  16.217 -               in  if k'+np' >= bnd 
  16.218 -		   then depth (bnd, Int.min(inc, k'+np'+1-bnd)) qs
  16.219 -		   else if np' < np (*solved a subgoal; prune rigid ancestors*)
  16.220 -                   then depth (bnd,inc) 
  16.221 -		         (prune ((k', np', rgd', tf st), (k,np,rgd,stq) :: qs))
  16.222 -	           else depth (bnd,inc) ((k', np', rgd', tf st) :: 
  16.223 -					 (k,np,rgd,stq) :: qs)
  16.224 -	       end
  16.225 +               in  if k'+np' >= bnd
  16.226 +                   then depth (bnd, Int.min(inc, k'+np'+1-bnd)) qs
  16.227 +                   else if np' < np (*solved a subgoal; prune rigid ancestors*)
  16.228 +                   then depth (bnd,inc)
  16.229 +                         (prune ((k', np', rgd', tf st), (k,np,rgd,stq) :: qs))
  16.230 +                   else depth (bnd,inc) ((k', np', rgd', tf st) ::
  16.231 +                                         (k,np,rgd,stq) :: qs)
  16.232 +               end
  16.233    in depth (0,5) [] end);
  16.234  
  16.235  val ITER_DEEPEN = THEN_ITER_DEEPEN all_tac;
  16.236 @@ -190,16 +190,16 @@
  16.237  
  16.238  (*Simple iterative deepening tactical.  It merely "deepens" any search tactic
  16.239    using increment "inc" up to limit "lim". *)
  16.240 -fun DEEPEN (inc,lim) tacf m i = 
  16.241 -  let fun dpn m st = 
  16.242 +fun DEEPEN (inc,lim) tacf m i =
  16.243 +  let fun dpn m st =
  16.244         st |> (if has_fewer_prems i st then no_tac
  16.245 -	      else if m>lim then 
  16.246 -		       (warning "Search depth limit exceeded: giving up"; 
  16.247 -			no_tac)
  16.248 -	      else (warning ("Search depth = " ^ string_of_int m);
  16.249 -			     tacf m i  ORELSE  dpn (m+inc)))
  16.250 +              else if m>lim then
  16.251 +                       (warning "Search depth limit exceeded: giving up";
  16.252 +                        no_tac)
  16.253 +              else (warning ("Search depth = " ^ string_of_int m);
  16.254 +                             tacf m i  ORELSE  dpn (m+inc)))
  16.255    in  dpn m  end;
  16.256 - 
  16.257 +
  16.258  (*** Best-first search ***)
  16.259  
  16.260  val trace_BEST_FIRST = ref false;
  16.261 @@ -209,7 +209,7 @@
  16.262    | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
  16.263  
  16.264  (*Check for and delete duplicate proof states*)
  16.265 -fun deleteAllMin prf heap = 
  16.266 +fun deleteAllMin prf heap =
  16.267        if ThmHeap.is_empty heap then heap
  16.268        else if Thm.eq_thm (prf, #2 (ThmHeap.min heap))
  16.269        then deleteAllMin prf (ThmHeap.delete_min heap)
  16.270 @@ -218,23 +218,22 @@
  16.271  (*Best-first search for a state that satisfies satp (incl initial state)
  16.272    Function sizef estimates size of problem remaining (smaller means better).
  16.273    tactic tac0 sets up the initial priority queue, while tac1 searches it. *)
  16.274 -fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 = 
  16.275 +fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 =
  16.276    let val tac = tracify trace_BEST_FIRST tac1
  16.277        fun pairsize th = (sizef th, th);
  16.278        fun bfs (news,nprf_heap) =
  16.279 -	   (case  List.partition satp news  of
  16.280 -		([],nonsats) => next(foldr ThmHeap.insert
  16.281 -					nprf_heap (map pairsize nonsats))
  16.282 -	      | (sats,_)  => some_of_list sats)
  16.283 +           (case  List.partition satp news  of
  16.284 +                ([],nonsats) => next(fold_rev ThmHeap.insert (map pairsize nonsats) nprf_heap)
  16.285 +              | (sats,_)  => some_of_list sats)
  16.286        and next nprf_heap =
  16.287              if ThmHeap.is_empty nprf_heap then NONE
  16.288 -	    else 
  16.289 -	    let val (n,prf) = ThmHeap.min nprf_heap
  16.290 -	    in if !trace_BEST_FIRST 
  16.291 -	       then tracing("state size = " ^ string_of_int n)  
  16.292 +            else
  16.293 +            let val (n,prf) = ThmHeap.min nprf_heap
  16.294 +            in if !trace_BEST_FIRST
  16.295 +               then tracing("state size = " ^ string_of_int n)
  16.296                 else ();
  16.297 -	       bfs (Seq.list_of (tac prf), 
  16.298 -		    deleteAllMin prf (ThmHeap.delete_min nprf_heap))
  16.299 +               bfs (Seq.list_of (tac prf),
  16.300 +                    deleteAllMin prf (ThmHeap.delete_min nprf_heap))
  16.301              end
  16.302        fun btac st = bfs (Seq.list_of (tac0 st), ThmHeap.empty)
  16.303    in traced_tac btac end;
  16.304 @@ -242,32 +241,32 @@
  16.305  (*Ordinary best-first search, with no initial tactic*)
  16.306  val BEST_FIRST = THEN_BEST_FIRST all_tac;
  16.307  
  16.308 -(*Breadth-first search to satisfy satpred (including initial state) 
  16.309 +(*Breadth-first search to satisfy satpred (including initial state)
  16.310    SLOW -- SHOULD NOT USE APPEND!*)
  16.311 -fun gen_BREADTH_FIRST message satpred (tac:tactic) = 
  16.312 +fun gen_BREADTH_FIRST message satpred (tac:tactic) =
  16.313    let val tacf = Seq.list_of o tac;
  16.314        fun bfs prfs =
  16.315 -	 (case  List.partition satpred prfs  of
  16.316 -	      ([],[]) => []
  16.317 -	    | ([],nonsats) => 
  16.318 -		  (message("breadth=" ^ string_of_int(length nonsats));
  16.319 -		   bfs (maps tacf nonsats))
  16.320 -	    | (sats,_)  => sats)
  16.321 +         (case  List.partition satpred prfs  of
  16.322 +              ([],[]) => []
  16.323 +            | ([],nonsats) =>
  16.324 +                  (message("breadth=" ^ string_of_int(length nonsats));
  16.325 +                   bfs (maps tacf nonsats))
  16.326 +            | (sats,_)  => sats)
  16.327    in (fn st => Seq.of_list (bfs [st])) end;
  16.328  
  16.329  val BREADTH_FIRST = gen_BREADTH_FIRST tracing;
  16.330  val QUIET_BREADTH_FIRST = gen_BREADTH_FIRST (K ());
  16.331  
  16.332  
  16.333 -(*  Author: 	Norbert Voelker, FernUniversitaet Hagen
  16.334 +(*  Author:     Norbert Voelker, FernUniversitaet Hagen
  16.335      Remarks:    Implementation of A*-like proof procedure by modification
  16.336 -		of the existing code for BEST_FIRST and best_tac so that the 
  16.337 -		current level of search is taken into account.
  16.338 -*)		
  16.339 +                of the existing code for BEST_FIRST and best_tac so that the
  16.340 +                current level of search is taken into account.
  16.341 +*)
  16.342  
  16.343  (*Insertion into priority queue of states, marked with level *)
  16.344  fun insert_with_level (lnth: int*int*thm, []) = [lnth]
  16.345 -  | insert_with_level ((l,m,th), (l',n,th')::nths) = 
  16.346 +  | insert_with_level ((l,m,th), (l',n,th')::nths) =
  16.347        if  n<m then (l',n,th') :: insert_with_level ((l,m,th), nths)
  16.348        else if  n=m andalso Thm.eq_thm(th,th')
  16.349                then (l',n,th')::nths
  16.350 @@ -277,23 +276,23 @@
  16.351  fun some_of_list []     = NONE
  16.352    | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
  16.353  
  16.354 -val trace_ASTAR = ref false; 
  16.355 +val trace_ASTAR = ref false;
  16.356  
  16.357 -fun THEN_ASTAR tac0 (satp, costf) tac1 = 
  16.358 -  let val tf = tracify trace_ASTAR tac1;   
  16.359 +fun THEN_ASTAR tac0 (satp, costf) tac1 =
  16.360 +  let val tf = tracify trace_ASTAR tac1;
  16.361        fun bfs (news,nprfs,level) =
  16.362        let fun cost thm = (level, costf level thm, thm)
  16.363        in (case  List.partition satp news  of
  16.364 -            ([],nonsats) 
  16.365 -		 => next (foldr insert_with_level nprfs (map cost nonsats))
  16.366 +            ([],nonsats)
  16.367 +                 => next (List.foldr insert_with_level nprfs (map cost nonsats))
  16.368            | (sats,_)  => some_of_list sats)
  16.369 -      end and    
  16.370 +      end and
  16.371        next []  = NONE
  16.372          | next ((level,n,prf)::nprfs)  =
  16.373 -            (if !trace_ASTAR 
  16.374 +            (if !trace_ASTAR
  16.375                 then tracing("level = " ^ string_of_int level ^
  16.376 -			 "  cost = " ^ string_of_int n ^ 
  16.377 -                         "  queue length =" ^ string_of_int (length nprfs))  
  16.378 +                         "  cost = " ^ string_of_int n ^
  16.379 +                         "  queue length =" ^ string_of_int (length nprfs))
  16.380                 else ();
  16.381               bfs (Seq.list_of (tf prf), nprfs,level+1))
  16.382        fun tf st = bfs (Seq.list_of (tac0 st), [], 0)
    17.1 --- a/src/Pure/tactic.ML	Thu May 31 23:02:16 2007 +0200
    17.2 +++ b/src/Pure/tactic.ML	Thu May 31 23:47:36 2007 +0200
    17.3 @@ -51,11 +51,11 @@
    17.4    val forward_tac       : thm list -> int -> tactic
    17.5    val forw_inst_tac     : (string*string)list -> thm -> int -> tactic
    17.6    val ftac              : thm -> int ->tactic
    17.7 -  val insert_tagged_brl : ('a * (bool * thm)) *
    17.8 -    (('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) ->
    17.9 +  val insert_tagged_brl : 'a * (bool * thm) ->
   17.10 +    ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
   17.11        ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
   17.12 -  val delete_tagged_brl : (bool * thm) *
   17.13 -    (('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) ->
   17.14 +  val delete_tagged_brl : bool * thm ->
   17.15 +    ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
   17.16        ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
   17.17    val lessb             : (bool * thm) * (bool * thm) -> bool
   17.18    val lift_inst_rule    : thm * int * (string*string)list * thm -> thm
   17.19 @@ -410,7 +410,7 @@
   17.20  fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls);
   17.21  
   17.22  (*insert one tagged brl into the pair of nets*)
   17.23 -fun insert_tagged_brl (kbrl as (k, (eres, th)), (inet, enet)) =
   17.24 +fun insert_tagged_brl (kbrl as (k, (eres, th))) (inet, enet) =
   17.25    if eres then
   17.26      (case try Thm.major_prem_of th of
   17.27        SOME prem => (inet, Net.insert_term (K false) (prem, kbrl) enet)
   17.28 @@ -419,12 +419,12 @@
   17.29  
   17.30  (*build a pair of nets for biresolution*)
   17.31  fun build_netpair netpair brls =
   17.32 -    foldr insert_tagged_brl netpair (taglist 1 brls);
   17.33 +    fold_rev insert_tagged_brl (taglist 1 brls) netpair;
   17.34  
   17.35  (*delete one kbrl from the pair of nets*)
   17.36  fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
   17.37  
   17.38 -fun delete_tagged_brl (brl as (eres, th), (inet, enet)) =
   17.39 +fun delete_tagged_brl (brl as (eres, th)) (inet, enet) =
   17.40    (if eres then
   17.41      (case try Thm.major_prem_of th of
   17.42        SOME prem => (inet, Net.delete_term eq_kbrl (prem, ((), brl)) enet)
   17.43 @@ -458,12 +458,12 @@
   17.44  (*** Simpler version for resolve_tac -- only one net, and no hyps ***)
   17.45  
   17.46  (*insert one tagged rl into the net*)
   17.47 -fun insert_krl (krl as (k,th), net) =
   17.48 -    Net.insert_term (K false) (concl_of th, krl) net;
   17.49 +fun insert_krl (krl as (k,th)) =
   17.50 +  Net.insert_term (K false) (concl_of th, krl);
   17.51  
   17.52  (*build a net of rules for resolution*)
   17.53  fun build_net rls =
   17.54 -    foldr insert_krl Net.empty (taglist 1 rls);
   17.55 +  fold_rev insert_krl (taglist 1 rls) Net.empty;
   17.56  
   17.57  (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
   17.58  fun filt_resolution_from_net_tac match pred net =
    18.1 --- a/src/Pure/tctical.ML	Thu May 31 23:02:16 2007 +0200
    18.2 +++ b/src/Pure/tctical.ML	Thu May 31 23:47:36 2007 +0200
    18.3 @@ -177,10 +177,10 @@
    18.4  fun EVERY1 tacs = EVERY' tacs 1;
    18.5  
    18.6  (* FIRST [tac1,...,tacn]   equals    tac1 ORELSE ... ORELSE tacn   *)
    18.7 -fun FIRST tacs = foldr (op ORELSE) no_tac tacs;
    18.8 +fun FIRST tacs = fold_rev (curry op ORELSE) tacs no_tac;
    18.9  
   18.10  (* FIRST' [tac1,...,tacn] i  equals    tac1 i ORELSE ... ORELSE tacn i   *)
   18.11 -fun FIRST' tacs = foldr (op ORELSE') (K no_tac) tacs;
   18.12 +fun FIRST' tacs = fold_rev (curry op ORELSE') tacs (K no_tac);
   18.13  
   18.14  (*Apply first tactic to 1*)
   18.15  fun FIRST1 tacs = FIRST' tacs 1;
   18.16 @@ -413,7 +413,7 @@
   18.17  (*Common code for METAHYPS and metahyps_thms*)
   18.18  fun metahyps_split_prem prem =
   18.19    let (*find all vars in the hyps -- should find tvars also!*)
   18.20 -      val hyps_vars = foldr add_term_vars [] (Logic.strip_assums_hyp prem)
   18.21 +      val hyps_vars = List.foldr add_term_vars [] (Logic.strip_assums_hyp prem)
   18.22        val insts = map mk_inst hyps_vars
   18.23        (*replace the hyps_vars by Frees*)
   18.24        val prem' = subst_atomic insts prem
   18.25 @@ -453,7 +453,7 @@
   18.26        fun relift st =
   18.27          let val prop = Thm.prop_of st
   18.28              val subgoal_vars = (*Vars introduced in the subgoals*)
   18.29 -                  foldr add_term_vars [] (Logic.strip_imp_prems prop)
   18.30 +                  List.foldr add_term_vars [] (Logic.strip_imp_prems prop)
   18.31              and concl_vars = add_term_vars (Logic.strip_imp_concl prop, [])
   18.32              val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
   18.33              val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
    19.1 --- a/src/Pure/term.ML	Thu May 31 23:02:16 2007 +0200
    19.2 +++ b/src/Pure/term.ML	Thu May 31 23:47:36 2007 +0200
    19.3 @@ -1112,20 +1112,20 @@
    19.4    | add_term_names (_, bs) = bs;
    19.5  
    19.6  (*Accumulates the TVars in a type, suppressing duplicates. *)
    19.7 -fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts
    19.8 +fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
    19.9    | add_typ_tvars(TFree(_),vs) = vs
   19.10    | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
   19.11  
   19.12  (*Accumulates the TFrees in a type, suppressing duplicates. *)
   19.13 -fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts
   19.14 +fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
   19.15    | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
   19.16    | add_typ_tfree_names(TVar(_),fs) = fs;
   19.17  
   19.18 -fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts
   19.19 +fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
   19.20    | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
   19.21    | add_typ_tfrees(TVar(_),fs) = fs;
   19.22  
   19.23 -fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts
   19.24 +fun add_typ_varnames(Type(_,Ts),nms) = List.foldr add_typ_varnames nms Ts
   19.25    | add_typ_varnames(TFree(nm,_),nms) = insert (op =) nm nms
   19.26    | add_typ_varnames(TVar((nm,_),_),nms) = insert (op =) nm nms;
   19.27  
    20.1 --- a/src/Pure/thm.ML	Thu May 31 23:02:16 2007 +0200
    20.2 +++ b/src/Pure/thm.ML	Thu May 31 23:47:36 2007 +0200
    20.3 @@ -1150,7 +1150,7 @@
    20.4  (* Replace all TFrees not fixed or in the hyps by new TVars *)
    20.5  fun varifyT' fixed (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...}) =
    20.6    let
    20.7 -    val tfrees = foldr add_term_tfrees fixed hyps;
    20.8 +    val tfrees = List.foldr add_term_tfrees fixed hyps;
    20.9      val prop1 = attach_tpairs tpairs prop;
   20.10      val (al, prop2) = Type.varify tfrees prop1;
   20.11      val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
   20.12 @@ -1430,7 +1430,7 @@
   20.13  
   20.14  (*Function to rename bounds/unknowns in the argument, lifted over B*)
   20.15  fun rename_bvars(dpairs, tpairs, B) =
   20.16 -        rename_bvs(foldr Term.match_bvars [] dpairs, dpairs, tpairs, B);
   20.17 +        rename_bvs(List.foldr Term.match_bvars [] dpairs, dpairs, tpairs, B);
   20.18  
   20.19  
   20.20  (*** RESOLUTION ***)
    21.1 --- a/src/Pure/type.ML	Thu May 31 23:02:16 2007 +0200
    21.2 +++ b/src/Pure/type.ML	Thu May 31 23:47:36 2007 +0200
    21.3 @@ -264,7 +264,7 @@
    21.4    let
    21.5      val used = add_typ_tfree_names (T, [])
    21.6      and tvars = map #1 (add_typ_tvars (T, []));
    21.7 -    val (alist, _) = foldr new_name ([], used) tvars;
    21.8 +    val (alist, _) = List.foldr new_name ([], used) tvars;
    21.9    in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
   21.10  
   21.11  val freeze_type = #1 o freeze_thaw_type;
   21.12 @@ -273,7 +273,7 @@
   21.13    let
   21.14      val used = it_term_types add_typ_tfree_names (t, [])
   21.15      and tvars = map #1 (it_term_types add_typ_tvars (t, []));
   21.16 -    val (alist, _) = foldr new_name ([], used) tvars;
   21.17 +    val (alist, _) = List.foldr new_name ([], used) tvars;
   21.18    in
   21.19      (case alist of
   21.20        [] => (t, fn x => x) (*nothing to do!*)
    22.1 --- a/src/Pure/unify.ML	Thu May 31 23:02:16 2007 +0200
    22.2 +++ b/src/Pure/unify.ML	Thu May 31 23:47:36 2007 +0200
    22.3 @@ -280,7 +280,7 @@
    22.4    Clever would be to re-do just the affected dpairs*)
    22.5  fun SIMPL thy (env,dpairs) : Envir.env * dpair list * dpair list =
    22.6      let val all as (env',flexflex,flexrigid) =
    22.7 -      foldr (SIMPL0 thy) (env,[],[]) dpairs;
    22.8 +      List.foldr (SIMPL0 thy) (env,[],[]) dpairs;
    22.9    val dps = flexrigid@flexflex
   22.10      in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps
   22.11         then SIMPL thy (env',dps) else all
   22.12 @@ -471,7 +471,7 @@
   22.13    val (Ts,U) = strip_type env T
   22.14    and js = length ts - 1  downto 0
   22.15    val args = sort (make_ord arg_less)
   22.16 -    (foldr (change_arg banned) [] (flexargs (js,ts,Ts)))
   22.17 +    (List.foldr (change_arg banned) [] (flexargs (js,ts,Ts)))
   22.18    val ts' = map (#t) args
   22.19      in
   22.20      if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
   22.21 @@ -504,7 +504,7 @@
   22.22              then  (bnos, (a,T)::newbinder)  (*needed by both: keep*)
   22.23              else  (j::bnos, newbinder);   (*remove*)
   22.24        val indices = 0 upto (length rbinder - 1);
   22.25 -      val (banned,rbin') = foldr add_index ([],[]) (rbinder~~indices);
   22.26 +      val (banned,rbin') = List.foldr add_index ([],[]) (rbinder~~indices);
   22.27        val (env', t') = clean_term banned (env, t);
   22.28        val (env'',u') = clean_term banned (env',u)
   22.29    in  (ff_assign thy (env'', rbin', t', u'), tpairs)
   22.30 @@ -558,7 +558,7 @@
   22.31      then print_dpairs thy "Enter SIMPL" (env,dpairs)  else ();
   22.32      SIMPL thy (env,dpairs))
   22.33      in case flexrigid of
   22.34 -        [] => SOME (foldr (add_ffpair thy) (env',[]) flexflex, reseq)
   22.35 +        [] => SOME (List.foldr (add_ffpair thy) (env',[]) flexflex, reseq)
   22.36        | dp::frigid' =>
   22.37      if tdepth > !search_bound then
   22.38          (warning "Unification bound exceeded"; Seq.pull reseq)
   22.39 @@ -607,7 +607,7 @@
   22.40  
   22.41  (*Smash all flex-flexpairs.  Should allow selection of pairs by a predicate?*)
   22.42  fun smash_flexflex (env,tpairs) : Envir.env =
   22.43 -  foldr smash_flexflex1 env tpairs;
   22.44 +  List.foldr smash_flexflex1 env tpairs;
   22.45  
   22.46  (*Returns unifiers with no remaining disagreement pairs*)
   22.47  fun smash_unifiers thy tus env =