tuned;
authorwenzelm
Wed Apr 26 22:38:05 2006 +0200 (2006-04-26)
changeset 19473d87a8838afa4
parent 19472 896eb8056e97
child 19474 70223ad97843
tuned;
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/typedef_package.ML
src/Provers/eqsubst.ML
src/Pure/General/file.ML
src/Pure/General/scan.ML
src/Pure/General/symbol.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/context_rules.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Proof/reconstruct.ML
src/Pure/Syntax/ast.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/Thy/thy_info.ML
src/Pure/codegen.ML
src/Pure/proof_general.ML
src/Pure/pure_thy.ML
src/Pure/tactic.ML
src/Pure/term.ML
src/Pure/unify.ML
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Apr 26 20:34:11 2006 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Apr 26 22:38:05 2006 +0200
     1.3 @@ -208,7 +208,7 @@
     1.4        else NONE) rss;
     1.5      val fs = List.concat (snd (foldl_map (fn (intrs, (prems, dummy)) =>
     1.6        let
     1.7 -        val (intrs1, intrs2) = splitAt (length prems, intrs);
     1.8 +        val (intrs1, intrs2) = chop (length prems) intrs;
     1.9          val fs = map (fn (rule, intr) =>
    1.10            fun_of_prem thy rsets vs params rule intr) (prems ~~ intrs1)
    1.11        in (intrs2, if dummy then Const ("arbitrary",
    1.12 @@ -330,7 +330,7 @@
    1.13        if s mem rsets then
    1.14          let
    1.15            val (d :: dummies') = dummies;
    1.16 -          val (recs1, recs2) = splitAt (length rs, if d then tl recs else recs)
    1.17 +          val (recs1, recs2) = chop (length rs) (if d then tl recs else recs)
    1.18          in ((recs2, dummies'), map (head_of o hd o rev o snd o strip_comb o
    1.19            fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1)
    1.20          end
     2.1 --- a/src/HOL/Tools/typedef_package.ML	Wed Apr 26 20:34:11 2006 +0200
     2.2 +++ b/src/HOL/Tools/typedef_package.ML	Wed Apr 26 22:38:05 2006 +0200
     2.3 @@ -119,11 +119,11 @@
     2.4      fun mk_nonempty A =
     2.5        HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
     2.6      val goal = mk_nonempty set;
     2.7 -    val goal_pat = mk_nonempty (Var (if_none (Syntax.read_variable name) (name, 0), setT));
     2.8 +    val goal_pat = mk_nonempty (Var (the_default (name, 0) (Syntax.read_variable name), setT));
     2.9  
    2.10      (*lhs*)
    2.11      val defS = Sign.defaultS thy;
    2.12 -    val lhs_tfrees = map (fn v => (v, if_none (AList.lookup (op =) rhs_tfrees v) defS)) vs;
    2.13 +    val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
    2.14      val args_setT = lhs_tfrees
    2.15        |> filter (member (op =) rhs_tfrees andf (not o member (op =) rhs_tfreesT))
    2.16        |> map TFree;
    2.17 @@ -132,7 +132,7 @@
    2.18      val full_tname = full tname;
    2.19      val newT = Type (full_tname, map TFree lhs_tfrees);
    2.20  
    2.21 -    val (Rep_name, Abs_name) = if_none opt_morphs ("Rep_" ^ name, "Abs_" ^ name);
    2.22 +    val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs;
    2.23      val setT' = map Term.itselfT args_setT ---> setT;
    2.24      val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT);
    2.25      val RepC = Const (full Rep_name, newT --> oldT);
    2.26 @@ -303,7 +303,7 @@
    2.27      Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
    2.28  
    2.29  fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
    2.30 -  typedef ((def, if_none opt_name (Syntax.type_name t mx)), (t, vs, mx), A, morphs);
    2.31 +  typedef ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
    2.32  
    2.33  val typedefP =
    2.34    OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
     3.1 --- a/src/Provers/eqsubst.ML	Wed Apr 26 20:34:11 2006 +0200
     3.2 +++ b/src/Provers/eqsubst.ML	Wed Apr 26 22:38:05 2006 +0200
     3.3 @@ -61,9 +61,8 @@
     3.4            in
     3.5            (case t' of
     3.6              (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
     3.7 -                       Seq.cons(f ft,
     3.8 -                                  maux (IsaFTerm.focus_right ft)))
     3.9 -          | (Abs _) => Seq.cons(f ft, maux (IsaFTerm.focus_abs ft))
    3.10 +                       Seq.cons (f ft) (maux (IsaFTerm.focus_right ft)))
    3.11 +          | (Abs _) => Seq.cons (f ft) (maux (IsaFTerm.focus_abs ft))
    3.12            | leaf => Seq.single (f ft)) end
    3.13      in maux ft end;
    3.14  
    3.15 @@ -76,10 +75,9 @@
    3.16            in
    3.17            (case (IsaFTerm.focus_of_fcterm ft) of
    3.18              (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
    3.19 -                       Seq.cons(hereseq,
    3.20 -                                  maux (IsaFTerm.focus_right ft)))
    3.21 -          | (Abs _) => Seq.cons(hereseq, maux (IsaFTerm.focus_abs ft))
    3.22 -          | leaf => Seq.single (hereseq))
    3.23 +                       Seq.cons hereseq (maux (IsaFTerm.focus_right ft)))
    3.24 +          | (Abs _) => Seq.cons hereseq (maux (IsaFTerm.focus_abs ft))
    3.25 +          | leaf => Seq.single hereseq)
    3.26            end
    3.27      in maux ft end;
    3.28  
     4.1 --- a/src/Pure/General/file.ML	Wed Apr 26 20:34:11 2006 +0200
     4.2 +++ b/src/Pure/General/file.ML	Wed Apr 26 22:38:05 2006 +0200
     4.3 @@ -103,7 +103,7 @@
     4.4  fun mkdir path = system_command ("mkdir -p " ^ shell_path path);
     4.5  
     4.6  fun is_dir path =
     4.7 -  if_none (try OS.FileSys.isDir (platform_path path)) false;
     4.8 +  the_default false (try OS.FileSys.isDir (platform_path path));
     4.9  
    4.10  
    4.11  (* read / write files *)
     5.1 --- a/src/Pure/General/scan.ML	Wed Apr 26 20:34:11 2006 +0200
     5.2 +++ b/src/Pure/General/scan.ML	Wed Apr 26 22:38:05 2006 +0200
     5.3 @@ -248,7 +248,7 @@
     5.4  
     5.5  fun drain def_prmpt get stopper scan ((state, xs), src) =
     5.6    (scan (state, xs), src) handle MORE prmpt =>
     5.7 -    (case get (if_none prmpt def_prmpt) src of
     5.8 +    (case get (the_default def_prmpt prmpt) src of
     5.9        ([], _) => (finite' stopper scan (state, xs), src)
    5.10      | (xs', src') => drain def_prmpt get stopper scan ((state, xs @ xs'), src'));
    5.11  
    5.12 @@ -258,7 +258,7 @@
    5.13  
    5.14      fun drain_loop recover inp =
    5.15        drain_with (catch scanner) inp handle FAIL msg =>
    5.16 -        (Output.error_msg (if_none msg "Syntax error."); drain_with recover inp);
    5.17 +        (Output.error_msg (the_default "Syntax error." msg); drain_with recover inp);
    5.18  
    5.19      val ((ys, (state', xs')), src') =
    5.20        (case (get def_prmpt src, opt_recover) of
     6.1 --- a/src/Pure/General/symbol.ML	Wed Apr 26 20:34:11 2006 +0200
     6.2 +++ b/src/Pure/General/symbol.ML	Wed Apr 26 22:38:05 2006 +0200
     6.3 @@ -499,7 +499,7 @@
     6.4    else if s = "\\<spacespace>" then 2
     6.5    else 1;
     6.6  
     6.7 -fun sym_length ss = Library.foldl (fn (n, s) => sym_len s + n) (0, ss);
     6.8 +fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
     6.9  
    6.10  fun symbol_output str =
    6.11    if chars_only str then default_output str
     7.1 --- a/src/Pure/Isar/attrib.ML	Wed Apr 26 20:34:11 2006 +0200
     7.2 +++ b/src/Pure/Isar/attrib.ML	Wed Apr 26 22:38:05 2006 +0200
     7.3 @@ -219,7 +219,7 @@
     7.4  fun the_type types xi = the (types xi)
     7.5    handle Option.Option => error_var "No such variable in theorem: " xi;
     7.6  
     7.7 -fun unify_types thy types ((unifier, maxidx), (xi, u)) =
     7.8 +fun unify_types thy types (xi, u) (unifier, maxidx) =
     7.9    let
    7.10      val T = the_type types xi;
    7.11      val U = Term.fastype_of u;
    7.12 @@ -283,7 +283,7 @@
    7.13  
    7.14      val types' = #1 (Drule.types_sorts thm');
    7.15      val unifier = map (apsnd snd) (Vartab.dest (#1
    7.16 -      (Library.foldl (unify_types thy types') ((Vartab.empty, 0), internal_insts))));
    7.17 +      (fold (unify_types thy types') internal_insts (Vartab.empty, 0))));
    7.18  
    7.19      val type_insts'' = map (typ_subst unifier) type_insts';
    7.20      val internal_insts'' = map (subst unifier) internal_insts;
     8.1 --- a/src/Pure/Isar/context_rules.ML	Wed Apr 26 20:34:11 2006 +0200
     8.2 +++ b/src/Pure/Isar/context_rules.ML	Wed Apr 26 22:38:05 2006 +0200
     8.3 @@ -108,9 +108,9 @@
     8.4        val rules = Library.merge (fn ((_, (k1, th1)), (_, (k2, th2))) =>
     8.5            k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) (rules1, rules2);
     8.6        val next = ~ (length rules);
     8.7 -      val netpairs = Library.foldl (fn (nps, (n, (w, ((i, b), th)))) =>
     8.8 -          nth_map i (curry insert_tagged_brl ((w, n), (b, th))) nps)
     8.9 -        (empty_netpairs, next upto ~1 ~~ rules);
    8.10 +      val netpairs = fold (fn (n, (w, ((i, b), th))) =>
    8.11 +          nth_map i (curry insert_tagged_brl ((w, n), (b, th))))
    8.12 +        (next upto ~1 ~~ rules) empty_netpairs;
    8.13      in make_rules (next - 1) rules netpairs wrappers end
    8.14  
    8.15    fun print generic (Rules {rules, ...}) =
     9.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Apr 26 20:34:11 2006 +0200
     9.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Wed Apr 26 22:38:05 2006 +0200
     9.3 @@ -200,7 +200,7 @@
     9.4          fun strip [] t = t
     9.5            | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
     9.6        in
     9.7 -        strip Ts (Library.foldl (uncurry lambda o Library.swap) (t', frees))
     9.8 +        strip Ts (fold lambda frees t')
     9.9        end;
    9.10  
    9.11      fun rew Ts (prf1 %% prf2) = rew Ts prf1 %% rew Ts prf2
    10.1 --- a/src/Pure/Proof/proof_syntax.ML	Wed Apr 26 20:34:11 2006 +0200
    10.2 +++ b/src/Pure/Proof/proof_syntax.ML	Wed Apr 26 22:38:05 2006 +0200
    10.3 @@ -97,7 +97,7 @@
    10.4      val thms' = map (apsnd Thm.full_prop_of) (PureThy.all_thms_of thy);
    10.5  
    10.6      val tab = Symtab.foldl (fn (tab, (key, ps)) =>
    10.7 -      let val prop = if_none (AList.lookup (op =) thms' key) (Bound 0)
    10.8 +      let val prop = the_default (Bound 0) (AList.lookup (op =) thms' key)
    10.9        in fst (foldr (fn ((prop', prf), x as (tab, i)) =>
   10.10          if prop <> prop' then
   10.11            (Symtab.update (key ^ "_" ^ string_of_int i, prf) tab, i+1)
   10.12 @@ -110,7 +110,7 @@
   10.13        | rename (prf % t) = rename prf % t
   10.14        | rename (prf' as PThm ((s, tags), prf, prop, Ts)) =
   10.15            let
   10.16 -            val prop' = if_none (AList.lookup (op =) thms' s) (Bound 0);
   10.17 +            val prop' = the_default (Bound 0) (AList.lookup (op =) thms' s);
   10.18              val ps = remove (op =) prop' (map fst (the (Symtab.lookup thms s)))
   10.19            in if prop = prop' then prf' else
   10.20              PThm ((s ^ "_" ^ string_of_int (length ps - find_index_eq prop ps), tags),
   10.21 @@ -180,16 +180,16 @@
   10.22  val Oraclet = Const ("Oracle", propT --> proofT);
   10.23  val MinProoft = Const ("MinProof", proofT);
   10.24  
   10.25 -val mk_tyapp = Library.foldl (fn (prf, T) => Const ("Appt",
   10.26 +val mk_tyapp = fold (fn T => fn prf => Const ("Appt",
   10.27    [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
   10.28  
   10.29  fun term_of _ (PThm ((name, _), _, _, NONE)) =
   10.30        Const (NameSpace.append "thm" name, proofT)
   10.31    | term_of _ (PThm ((name, _), _, _, SOME Ts)) =
   10.32 -      mk_tyapp (Const (NameSpace.append "thm" name, proofT), Ts)
   10.33 +      mk_tyapp Ts (Const (NameSpace.append "thm" name, proofT))
   10.34    | term_of _ (PAxm (name, _, NONE)) = Const (NameSpace.append "axm" name, proofT)
   10.35    | term_of _ (PAxm (name, _, SOME Ts)) =
   10.36 -      mk_tyapp (Const (NameSpace.append "axm" name, proofT), Ts)
   10.37 +      mk_tyapp Ts (Const (NameSpace.append "axm" name, proofT))
   10.38    | term_of _ (PBound i) = Bound i
   10.39    | term_of Ts (Abst (s, opT, prf)) = 
   10.40        let val T = the_default dummyT opT
    11.1 --- a/src/Pure/Proof/reconstruct.ML	Wed Apr 26 20:34:11 2006 +0200
    11.2 +++ b/src/Pure/Proof/reconstruct.ML	Wed Apr 26 22:38:05 2006 +0200
    11.3 @@ -57,7 +57,7 @@
    11.4    (Envir.Envir {iTs = iTs, asol = asol, maxidx = maxidx+1},
    11.5     TVar (("'t", maxidx+1), s));
    11.6  
    11.7 -fun mk_abs Ts t = Library.foldl (fn (u, T) => Abs ("", T, u)) (t, Ts);
    11.8 +val mk_abs = fold (fn T => fn u => Abs ("", T, u));
    11.9  
   11.10  fun unifyT sg env T U =
   11.11    let
    12.1 --- a/src/Pure/Syntax/ast.ML	Wed Apr 26 20:34:11 2006 +0200
    12.2 +++ b/src/Pure/Syntax/ast.ML	Wed Apr 26 22:38:05 2006 +0200
    12.3 @@ -129,7 +129,7 @@
    12.4    | fold_ast _ [y] = y
    12.5    | fold_ast c (x :: xs) = Appl [Constant c, x, fold_ast c xs];
    12.6  
    12.7 -fun fold_ast_p c = Library.foldr (fn (x, xs) => Appl [Constant c, x, xs]);
    12.8 +fun fold_ast_p c = uncurry (fold_rev (fn x => fn xs => Appl [Constant c, x, xs]));
    12.9  
   12.10  
   12.11  (* unfold asts *)
    13.1 --- a/src/Pure/Syntax/syn_trans.ML	Wed Apr 26 20:34:11 2006 +0200
    13.2 +++ b/src/Pure/Syntax/syn_trans.ML	Wed Apr 26 22:38:05 2006 +0200
    13.3 @@ -276,7 +276,7 @@
    13.4  
    13.5  
    13.6  fun abs_tr' tm =
    13.7 -  Library.foldr (fn (x, t) => Lexicon.const "_abs" $ x $ t)
    13.8 +  uncurry (fold_rev (fn x => fn t => Lexicon.const "_abs" $ x $ t))
    13.9      (strip_abss strip_abs_vars strip_abs_body (eta_contr tm));
   13.10  
   13.11  fun atomic_abs_tr' (x, T, t) =
    14.1 --- a/src/Pure/Thy/thy_info.ML	Wed Apr 26 20:34:11 2006 +0200
    14.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Apr 26 22:38:05 2006 +0200
    14.3 @@ -86,7 +86,7 @@
    14.4    handle Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));
    14.5  
    14.6  fun upd_deps name entry G =
    14.7 -  Library.foldl (fn (H, parent) => Graph.del_edge (parent, name) H) (G, Graph.imm_preds G name)
    14.8 +  fold (fn parent => Graph.del_edge (parent, name)) (Graph.imm_preds G name) G
    14.9    |> Graph.map_node name (K entry);
   14.10  
   14.11  fun update_node name parents entry G =
   14.12 @@ -243,8 +243,8 @@
   14.13  (* load_file *)
   14.14  
   14.15  val opt_path = Option.map (Path.dir o fst o ThyLoad.get_thy);
   14.16 -fun opt_path' (d: deps option) = if_none (Option.map (opt_path o #master) d) NONE;
   14.17 -fun opt_path'' d = if_none (Option.map opt_path' d) NONE;
   14.18 +fun opt_path' (d: deps option) = the_default NONE (Option.map (opt_path o #master) d);
   14.19 +fun opt_path'' d = the_default NONE (Option.map opt_path' d);
   14.20  
   14.21  local
   14.22  
   14.23 @@ -360,7 +360,7 @@
   14.24            handle ERROR msg => cat_error msg
   14.25              (loader_msg "the error(s) above occurred while examining theory" [name] ^
   14.26                (if null initiators then "" else required_by "\n" initiators));
   14.27 -        val dir' = if_none (opt_path'' new_deps) dir;
   14.28 +        val dir' = the_default dir (opt_path'' new_deps);
   14.29          val (visited', parent_results) = foldl_map (req_parent dir') (name :: visited, parents);
   14.30  
   14.31          val thy = if not really then SOME (get_theory name) else NONE;
   14.32 @@ -424,7 +424,7 @@
   14.33    let
   14.34      val bparents = map base_of_path parents;
   14.35      val dir' = opt_path'' (lookup_deps name);
   14.36 -    val dir = if_none dir' Path.current;
   14.37 +    val dir = the_default Path.current dir';
   14.38      val assert_thy = if int then quiet_update_thy' true dir else weak_use_thy dir;
   14.39      val _ = check_unfinished error name;
   14.40      val _ = List.app assert_thy parents;
    15.1 --- a/src/Pure/codegen.ML	Wed Apr 26 20:34:11 2006 +0200
    15.2 +++ b/src/Pure/codegen.ML	Wed Apr 26 22:38:05 2006 +0200
    15.3 @@ -516,12 +516,12 @@
    15.4  
    15.5  fun theory_of_type s thy =
    15.6    if Sign.declared_tyname thy s
    15.7 -  then SOME (if_none (get_first (theory_of_type s) (Theory.parents_of thy)) thy)
    15.8 +  then SOME (the_default thy (get_first (theory_of_type s) (Theory.parents_of thy)))
    15.9    else NONE;
   15.10  
   15.11  fun theory_of_const s thy =
   15.12    if Sign.declared_const thy s
   15.13 -  then SOME (if_none (get_first (theory_of_const s) (Theory.parents_of thy)) thy)
   15.14 +  then SOME (the_default thy (get_first (theory_of_const s) (Theory.parents_of thy)))
   15.15    else NONE;
   15.16  
   15.17  fun thyname_of_type s thy = (case theory_of_type s thy of
   15.18 @@ -587,7 +587,7 @@
   15.19            NONE => defs
   15.20          | SOME (s, (T, (args, rhs))) => Symtab.update
   15.21              (s, (T, (thyname, split_last (rename_terms (args @ [rhs])))) ::
   15.22 -            if_none (Symtab.lookup defs s) []) defs))
   15.23 +            the_default [] (Symtab.lookup defs s)) defs))
   15.24    in
   15.25      foldl (fn ((thyname, axms), defs) =>
   15.26        Symtab.foldl (add_def thyname) (defs, axms)) Symtab.empty axmss
    16.1 --- a/src/Pure/proof_general.ML	Wed Apr 26 20:34:11 2006 +0200
    16.2 +++ b/src/Pure/proof_general.ML	Wed Apr 26 22:38:05 2006 +0200
    16.3 @@ -172,12 +172,12 @@
    16.4          ("class",  pgip_class),
    16.5          ("seq",    string_of_int (pgip_serial())),
    16.6          ("id",     !pgip_id)] @
    16.7 -       if_none (Option.map (single o (pair "destid")) (! pgip_refid)) [] @
    16.8 +       the_default [] (Option.map (single o (pair "destid")) (! pgip_refid)) @
    16.9         (* destid=refid since Isabelle only communicates back to sender,
   16.10            so we may omit refid from attributes.
   16.11 -       if_none (Option.map (single o (pair "refid"))  (! pgip_refid)) [] @
   16.12 +       the_default [] (Option.map (single o (pair "refid"))  (! pgip_refid)) @
   16.13         *)
   16.14 -       if_none (Option.map (single o (pair "refseq")) (! pgip_refseq)) [])
   16.15 +       the_default [] (Option.map (single o (pair "refseq")) (! pgip_refseq)))
   16.16        pgips;
   16.17  
   16.18  in
   16.19 @@ -1102,7 +1102,7 @@
   16.20                                                ("default", default)]
   16.21                         [ty]) prefs)]) (!preferences)
   16.22  
   16.23 -fun allprefs () = Library.foldl (op @) ([], map snd (!preferences))
   16.24 +fun allprefs () = maps snd (!preferences)
   16.25  
   16.26  fun setpref name value =
   16.27      (case AList.lookup (op =) (allprefs ()) name of
    17.1 --- a/src/Pure/pure_thy.ML	Wed Apr 26 20:34:11 2006 +0200
    17.2 +++ b/src/Pure/pure_thy.ML	Wed Apr 26 22:38:05 2006 +0200
    17.3 @@ -415,8 +415,8 @@
    17.4        fst (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm))
    17.5    | smart_store name_thm (name, thms) =
    17.6        let
    17.7 -        fun merge (thy, th) = Theory.merge (thy, Thm.theory_of_thm th);
    17.8 -        val thy = Library.foldl merge (Thm.theory_of_thm (hd thms), tl thms);
    17.9 +        fun merge th thy = Theory.merge (thy, Thm.theory_of_thm th);
   17.10 +        val thy = fold merge (tl thms) (Thm.theory_of_thm (hd thms));
   17.11        in fst (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end;
   17.12  
   17.13  in
    18.1 --- a/src/Pure/tactic.ML	Wed Apr 26 20:34:11 2006 +0200
    18.2 +++ b/src/Pure/tactic.ML	Wed Apr 26 22:38:05 2006 +0200
    18.3 @@ -577,7 +577,7 @@
    18.4  
    18.5  val rev_defs = sort_lhs_depths o map symmetric;
    18.6  
    18.7 -fun fold_rule defs thm = Library.foldl (fn (th, ds) => rewrite_rule ds th) (thm, rev_defs defs);
    18.8 +fun fold_rule defs = fold rewrite_rule (rev_defs defs);
    18.9  fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
   18.10  fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
   18.11  
   18.12 @@ -628,12 +628,12 @@
   18.13  fun filter_prems_tac p =
   18.14    let fun Then NONE tac = SOME tac
   18.15          | Then (SOME tac) tac' = SOME(tac THEN' tac');
   18.16 -      fun thins ((tac,n),H) =
   18.17 +      fun thins H (tac,n) =
   18.18          if p H then (tac,n+1)
   18.19          else (Then tac (rotate_tac n THEN' etac thin_rl),0);
   18.20    in SUBGOAL(fn (subg,n) =>
   18.21         let val Hs = Logic.strip_assums_hyp subg
   18.22 -       in case fst(Library.foldl thins ((NONE,0),Hs)) of
   18.23 +       in case fst(fold thins Hs (NONE,0)) of
   18.24              NONE => no_tac | SOME tac => tac n
   18.25         end)
   18.26    end;
    19.1 --- a/src/Pure/term.ML	Wed Apr 26 20:34:11 2006 +0200
    19.2 +++ b/src/Pure/term.ML	Wed Apr 26 22:38:05 2006 +0200
    19.3 @@ -390,7 +390,7 @@
    19.4    in arg 0 [] tm end;
    19.5  
    19.6  
    19.7 -val list_abs = Library.foldr (fn ((x, T), t) => Abs (x, T, t));
    19.8 +val list_abs = uncurry (fold_rev (fn (x, T) => fn t => Abs (x, T, t)));
    19.9  
   19.10  fun strip_abs (Abs (a, T, t)) =
   19.11        let val (a', t') = strip_abs t
    20.1 --- a/src/Pure/unify.ML	Wed Apr 26 20:34:11 2006 +0200
    20.2 +++ b/src/Pure/unify.ML	Wed Apr 26 22:38:05 2006 +0200
    20.3 @@ -325,7 +325,7 @@
    20.4  	    (mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg),
    20.5  		 (env, dpairs)));
    20.6  	(*Produce sequence of all possible ways of copying the arg list*)
    20.7 -    fun copyargs [] = Seq.cons( ([],ed), Seq.empty)
    20.8 +    fun copyargs [] = Seq.cons ([],ed) Seq.empty
    20.9        | copyargs (uarg::uargs) = Seq.maps (copycons uarg) (copyargs uargs);
   20.10      val (uhead,uargs) = strip_comb u;
   20.11      val base = body_type env (fastype env (rbinder,uhead));
   20.12 @@ -577,7 +577,7 @@
   20.13    in add_unify 1 ((env, dps), Seq.empty) end;
   20.14  
   20.15  fun unifiers (params as (thy, env, tus)) =
   20.16 -  Seq.cons ((fold (Pattern.unify thy) tus env, []), Seq.empty)
   20.17 +  Seq.cons (fold (Pattern.unify thy) tus env, []) Seq.empty
   20.18      handle Pattern.Unif => Seq.empty
   20.19           | Pattern.Pattern => hounifiers params;
   20.20