# HG changeset patch
# User wenzelm
# Date 1146083885 -7200
# Node ID d87a8838afa4117372f1b12f286f44b3536bc892
# Parent  896eb8056e97d4f45578d0eec1c9e11d48a5b8a0
tuned;

diff -r 896eb8056e97 -r d87a8838afa4 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -208,7 +208,7 @@
       else NONE) rss;
     val fs = List.concat (snd (foldl_map (fn (intrs, (prems, dummy)) =>
       let
-        val (intrs1, intrs2) = splitAt (length prems, intrs);
+        val (intrs1, intrs2) = chop (length prems) intrs;
         val fs = map (fn (rule, intr) =>
           fun_of_prem thy rsets vs params rule intr) (prems ~~ intrs1)
       in (intrs2, if dummy then Const ("arbitrary",
@@ -330,7 +330,7 @@
       if s mem rsets then
         let
           val (d :: dummies') = dummies;
-          val (recs1, recs2) = splitAt (length rs, if d then tl recs else recs)
+          val (recs1, recs2) = chop (length rs) (if d then tl recs else recs)
         in ((recs2, dummies'), map (head_of o hd o rev o snd o strip_comb o
           fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1)
         end
diff -r 896eb8056e97 -r d87a8838afa4 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -119,11 +119,11 @@
     fun mk_nonempty A =
       HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
     val goal = mk_nonempty set;
-    val goal_pat = mk_nonempty (Var (if_none (Syntax.read_variable name) (name, 0), setT));
+    val goal_pat = mk_nonempty (Var (the_default (name, 0) (Syntax.read_variable name), setT));
 
     (*lhs*)
     val defS = Sign.defaultS thy;
-    val lhs_tfrees = map (fn v => (v, if_none (AList.lookup (op =) rhs_tfrees v) defS)) vs;
+    val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
     val args_setT = lhs_tfrees
       |> filter (member (op =) rhs_tfrees andf (not o member (op =) rhs_tfreesT))
       |> map TFree;
@@ -132,7 +132,7 @@
     val full_tname = full tname;
     val newT = Type (full_tname, map TFree lhs_tfrees);
 
-    val (Rep_name, Abs_name) = if_none opt_morphs ("Rep_" ^ name, "Abs_" ^ name);
+    val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs;
     val setT' = map Term.itselfT args_setT ---> setT;
     val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT);
     val RepC = Const (full Rep_name, newT --> oldT);
@@ -303,7 +303,7 @@
     Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
 
 fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
-  typedef ((def, if_none opt_name (Syntax.type_name t mx)), (t, vs, mx), A, morphs);
+  typedef ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
 
 val typedefP =
   OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
diff -r 896eb8056e97 -r d87a8838afa4 src/Provers/eqsubst.ML
--- a/src/Provers/eqsubst.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Provers/eqsubst.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -61,9 +61,8 @@
           in
           (case t' of
             (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
-                       Seq.cons(f ft,
-                                  maux (IsaFTerm.focus_right ft)))
-          | (Abs _) => Seq.cons(f ft, maux (IsaFTerm.focus_abs ft))
+                       Seq.cons (f ft) (maux (IsaFTerm.focus_right ft)))
+          | (Abs _) => Seq.cons (f ft) (maux (IsaFTerm.focus_abs ft))
           | leaf => Seq.single (f ft)) end
     in maux ft end;
 
@@ -76,10 +75,9 @@
           in
           (case (IsaFTerm.focus_of_fcterm ft) of
             (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
-                       Seq.cons(hereseq,
-                                  maux (IsaFTerm.focus_right ft)))
-          | (Abs _) => Seq.cons(hereseq, maux (IsaFTerm.focus_abs ft))
-          | leaf => Seq.single (hereseq))
+                       Seq.cons hereseq (maux (IsaFTerm.focus_right ft)))
+          | (Abs _) => Seq.cons hereseq (maux (IsaFTerm.focus_abs ft))
+          | leaf => Seq.single hereseq)
           end
     in maux ft end;
 
diff -r 896eb8056e97 -r d87a8838afa4 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/General/file.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -103,7 +103,7 @@
 fun mkdir path = system_command ("mkdir -p " ^ shell_path path);
 
 fun is_dir path =
-  if_none (try OS.FileSys.isDir (platform_path path)) false;
+  the_default false (try OS.FileSys.isDir (platform_path path));
 
 
 (* read / write files *)
diff -r 896eb8056e97 -r d87a8838afa4 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/General/scan.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -248,7 +248,7 @@
 
 fun drain def_prmpt get stopper scan ((state, xs), src) =
   (scan (state, xs), src) handle MORE prmpt =>
-    (case get (if_none prmpt def_prmpt) src of
+    (case get (the_default def_prmpt prmpt) src of
       ([], _) => (finite' stopper scan (state, xs), src)
     | (xs', src') => drain def_prmpt get stopper scan ((state, xs @ xs'), src'));
 
@@ -258,7 +258,7 @@
 
     fun drain_loop recover inp =
       drain_with (catch scanner) inp handle FAIL msg =>
-        (Output.error_msg (if_none msg "Syntax error."); drain_with recover inp);
+        (Output.error_msg (the_default "Syntax error." msg); drain_with recover inp);
 
     val ((ys, (state', xs')), src') =
       (case (get def_prmpt src, opt_recover) of
diff -r 896eb8056e97 -r d87a8838afa4 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/General/symbol.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -499,7 +499,7 @@
   else if s = "\\<spacespace>" then 2
   else 1;
 
-fun sym_length ss = Library.foldl (fn (n, s) => sym_len s + n) (0, ss);
+fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
 
 fun symbol_output str =
   if chars_only str then default_output str
diff -r 896eb8056e97 -r d87a8838afa4 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/Isar/attrib.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -219,7 +219,7 @@
 fun the_type types xi = the (types xi)
   handle Option.Option => error_var "No such variable in theorem: " xi;
 
-fun unify_types thy types ((unifier, maxidx), (xi, u)) =
+fun unify_types thy types (xi, u) (unifier, maxidx) =
   let
     val T = the_type types xi;
     val U = Term.fastype_of u;
@@ -283,7 +283,7 @@
 
     val types' = #1 (Drule.types_sorts thm');
     val unifier = map (apsnd snd) (Vartab.dest (#1
-      (Library.foldl (unify_types thy types') ((Vartab.empty, 0), internal_insts))));
+      (fold (unify_types thy types') internal_insts (Vartab.empty, 0))));
 
     val type_insts'' = map (typ_subst unifier) type_insts';
     val internal_insts'' = map (subst unifier) internal_insts;
diff -r 896eb8056e97 -r d87a8838afa4 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/Isar/context_rules.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -108,9 +108,9 @@
       val rules = Library.merge (fn ((_, (k1, th1)), (_, (k2, th2))) =>
           k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) (rules1, rules2);
       val next = ~ (length rules);
-      val netpairs = Library.foldl (fn (nps, (n, (w, ((i, b), th)))) =>
-          nth_map i (curry insert_tagged_brl ((w, n), (b, th))) nps)
-        (empty_netpairs, next upto ~1 ~~ rules);
+      val netpairs = fold (fn (n, (w, ((i, b), th))) =>
+          nth_map i (curry insert_tagged_brl ((w, n), (b, th))))
+        (next upto ~1 ~~ rules) empty_netpairs;
     in make_rules (next - 1) rules netpairs wrappers end
 
   fun print generic (Rules {rules, ...}) =
diff -r 896eb8056e97 -r d87a8838afa4 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -200,7 +200,7 @@
         fun strip [] t = t
           | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
       in
-        strip Ts (Library.foldl (uncurry lambda o Library.swap) (t', frees))
+        strip Ts (fold lambda frees t')
       end;
 
     fun rew Ts (prf1 %% prf2) = rew Ts prf1 %% rew Ts prf2
diff -r 896eb8056e97 -r d87a8838afa4 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -97,7 +97,7 @@
     val thms' = map (apsnd Thm.full_prop_of) (PureThy.all_thms_of thy);
 
     val tab = Symtab.foldl (fn (tab, (key, ps)) =>
-      let val prop = if_none (AList.lookup (op =) thms' key) (Bound 0)
+      let val prop = the_default (Bound 0) (AList.lookup (op =) thms' key)
       in fst (foldr (fn ((prop', prf), x as (tab, i)) =>
         if prop <> prop' then
           (Symtab.update (key ^ "_" ^ string_of_int i, prf) tab, i+1)
@@ -110,7 +110,7 @@
       | rename (prf % t) = rename prf % t
       | rename (prf' as PThm ((s, tags), prf, prop, Ts)) =
           let
-            val prop' = if_none (AList.lookup (op =) thms' s) (Bound 0);
+            val prop' = the_default (Bound 0) (AList.lookup (op =) thms' s);
             val ps = remove (op =) prop' (map fst (the (Symtab.lookup thms s)))
           in if prop = prop' then prf' else
             PThm ((s ^ "_" ^ string_of_int (length ps - find_index_eq prop ps), tags),
@@ -180,16 +180,16 @@
 val Oraclet = Const ("Oracle", propT --> proofT);
 val MinProoft = Const ("MinProof", proofT);
 
-val mk_tyapp = Library.foldl (fn (prf, T) => Const ("Appt",
+val mk_tyapp = fold (fn T => fn prf => Const ("Appt",
   [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
 
 fun term_of _ (PThm ((name, _), _, _, NONE)) =
       Const (NameSpace.append "thm" name, proofT)
   | term_of _ (PThm ((name, _), _, _, SOME Ts)) =
-      mk_tyapp (Const (NameSpace.append "thm" name, proofT), Ts)
+      mk_tyapp Ts (Const (NameSpace.append "thm" name, proofT))
   | term_of _ (PAxm (name, _, NONE)) = Const (NameSpace.append "axm" name, proofT)
   | term_of _ (PAxm (name, _, SOME Ts)) =
-      mk_tyapp (Const (NameSpace.append "axm" name, proofT), Ts)
+      mk_tyapp Ts (Const (NameSpace.append "axm" name, proofT))
   | term_of _ (PBound i) = Bound i
   | term_of Ts (Abst (s, opT, prf)) = 
       let val T = the_default dummyT opT
diff -r 896eb8056e97 -r d87a8838afa4 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -57,7 +57,7 @@
   (Envir.Envir {iTs = iTs, asol = asol, maxidx = maxidx+1},
    TVar (("'t", maxidx+1), s));
 
-fun mk_abs Ts t = Library.foldl (fn (u, T) => Abs ("", T, u)) (t, Ts);
+val mk_abs = fold (fn T => fn u => Abs ("", T, u));
 
 fun unifyT sg env T U =
   let
diff -r 896eb8056e97 -r d87a8838afa4 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/Syntax/ast.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -129,7 +129,7 @@
   | fold_ast _ [y] = y
   | fold_ast c (x :: xs) = Appl [Constant c, x, fold_ast c xs];
 
-fun fold_ast_p c = Library.foldr (fn (x, xs) => Appl [Constant c, x, xs]);
+fun fold_ast_p c = uncurry (fold_rev (fn x => fn xs => Appl [Constant c, x, xs]));
 
 
 (* unfold asts *)
diff -r 896eb8056e97 -r d87a8838afa4 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -276,7 +276,7 @@
 
 
 fun abs_tr' tm =
-  Library.foldr (fn (x, t) => Lexicon.const "_abs" $ x $ t)
+  uncurry (fold_rev (fn x => fn t => Lexicon.const "_abs" $ x $ t))
     (strip_abss strip_abs_vars strip_abs_body (eta_contr tm));
 
 fun atomic_abs_tr' (x, T, t) =
diff -r 896eb8056e97 -r d87a8838afa4 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -86,7 +86,7 @@
   handle Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));
 
 fun upd_deps name entry G =
-  Library.foldl (fn (H, parent) => Graph.del_edge (parent, name) H) (G, Graph.imm_preds G name)
+  fold (fn parent => Graph.del_edge (parent, name)) (Graph.imm_preds G name) G
   |> Graph.map_node name (K entry);
 
 fun update_node name parents entry G =
@@ -243,8 +243,8 @@
 (* load_file *)
 
 val opt_path = Option.map (Path.dir o fst o ThyLoad.get_thy);
-fun opt_path' (d: deps option) = if_none (Option.map (opt_path o #master) d) NONE;
-fun opt_path'' d = if_none (Option.map opt_path' d) NONE;
+fun opt_path' (d: deps option) = the_default NONE (Option.map (opt_path o #master) d);
+fun opt_path'' d = the_default NONE (Option.map opt_path' d);
 
 local
 
@@ -360,7 +360,7 @@
           handle ERROR msg => cat_error msg
             (loader_msg "the error(s) above occurred while examining theory" [name] ^
               (if null initiators then "" else required_by "\n" initiators));
-        val dir' = if_none (opt_path'' new_deps) dir;
+        val dir' = the_default dir (opt_path'' new_deps);
         val (visited', parent_results) = foldl_map (req_parent dir') (name :: visited, parents);
 
         val thy = if not really then SOME (get_theory name) else NONE;
@@ -424,7 +424,7 @@
   let
     val bparents = map base_of_path parents;
     val dir' = opt_path'' (lookup_deps name);
-    val dir = if_none dir' Path.current;
+    val dir = the_default Path.current dir';
     val assert_thy = if int then quiet_update_thy' true dir else weak_use_thy dir;
     val _ = check_unfinished error name;
     val _ = List.app assert_thy parents;
diff -r 896eb8056e97 -r d87a8838afa4 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/codegen.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -516,12 +516,12 @@
 
 fun theory_of_type s thy =
   if Sign.declared_tyname thy s
-  then SOME (if_none (get_first (theory_of_type s) (Theory.parents_of thy)) thy)
+  then SOME (the_default thy (get_first (theory_of_type s) (Theory.parents_of thy)))
   else NONE;
 
 fun theory_of_const s thy =
   if Sign.declared_const thy s
-  then SOME (if_none (get_first (theory_of_const s) (Theory.parents_of thy)) thy)
+  then SOME (the_default thy (get_first (theory_of_const s) (Theory.parents_of thy)))
   else NONE;
 
 fun thyname_of_type s thy = (case theory_of_type s thy of
@@ -587,7 +587,7 @@
           NONE => defs
         | SOME (s, (T, (args, rhs))) => Symtab.update
             (s, (T, (thyname, split_last (rename_terms (args @ [rhs])))) ::
-            if_none (Symtab.lookup defs s) []) defs))
+            the_default [] (Symtab.lookup defs s)) defs))
   in
     foldl (fn ((thyname, axms), defs) =>
       Symtab.foldl (add_def thyname) (defs, axms)) Symtab.empty axmss
diff -r 896eb8056e97 -r d87a8838afa4 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/proof_general.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -172,12 +172,12 @@
         ("class",  pgip_class),
         ("seq",    string_of_int (pgip_serial())),
         ("id",     !pgip_id)] @
-       if_none (Option.map (single o (pair "destid")) (! pgip_refid)) [] @
+       the_default [] (Option.map (single o (pair "destid")) (! pgip_refid)) @
        (* destid=refid since Isabelle only communicates back to sender,
           so we may omit refid from attributes.
-       if_none (Option.map (single o (pair "refid"))  (! pgip_refid)) [] @
+       the_default [] (Option.map (single o (pair "refid"))  (! pgip_refid)) @
        *)
-       if_none (Option.map (single o (pair "refseq")) (! pgip_refseq)) [])
+       the_default [] (Option.map (single o (pair "refseq")) (! pgip_refseq)))
       pgips;
 
 in
@@ -1102,7 +1102,7 @@
                                               ("default", default)]
                        [ty]) prefs)]) (!preferences)
 
-fun allprefs () = Library.foldl (op @) ([], map snd (!preferences))
+fun allprefs () = maps snd (!preferences)
 
 fun setpref name value =
     (case AList.lookup (op =) (allprefs ()) name of
diff -r 896eb8056e97 -r d87a8838afa4 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/pure_thy.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -415,8 +415,8 @@
       fst (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm))
   | smart_store name_thm (name, thms) =
       let
-        fun merge (thy, th) = Theory.merge (thy, Thm.theory_of_thm th);
-        val thy = Library.foldl merge (Thm.theory_of_thm (hd thms), tl thms);
+        fun merge th thy = Theory.merge (thy, Thm.theory_of_thm th);
+        val thy = fold merge (tl thms) (Thm.theory_of_thm (hd thms));
       in fst (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end;
 
 in
diff -r 896eb8056e97 -r d87a8838afa4 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/tactic.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -577,7 +577,7 @@
 
 val rev_defs = sort_lhs_depths o map symmetric;
 
-fun fold_rule defs thm = Library.foldl (fn (th, ds) => rewrite_rule ds th) (thm, rev_defs defs);
+fun fold_rule defs = fold rewrite_rule (rev_defs defs);
 fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
 fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
 
@@ -628,12 +628,12 @@
 fun filter_prems_tac p =
   let fun Then NONE tac = SOME tac
         | Then (SOME tac) tac' = SOME(tac THEN' tac');
-      fun thins ((tac,n),H) =
+      fun thins H (tac,n) =
         if p H then (tac,n+1)
         else (Then tac (rotate_tac n THEN' etac thin_rl),0);
   in SUBGOAL(fn (subg,n) =>
        let val Hs = Logic.strip_assums_hyp subg
-       in case fst(Library.foldl thins ((NONE,0),Hs)) of
+       in case fst(fold thins Hs (NONE,0)) of
             NONE => no_tac | SOME tac => tac n
        end)
   end;
diff -r 896eb8056e97 -r d87a8838afa4 src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/term.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -390,7 +390,7 @@
   in arg 0 [] tm end;
 
 
-val list_abs = Library.foldr (fn ((x, T), t) => Abs (x, T, t));
+val list_abs = uncurry (fold_rev (fn (x, T) => fn t => Abs (x, T, t)));
 
 fun strip_abs (Abs (a, T, t)) =
       let val (a', t') = strip_abs t
diff -r 896eb8056e97 -r d87a8838afa4 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Wed Apr 26 20:34:11 2006 +0200
+++ b/src/Pure/unify.ML	Wed Apr 26 22:38:05 2006 +0200
@@ -325,7 +325,7 @@
 	    (mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg),
 		 (env, dpairs)));
 	(*Produce sequence of all possible ways of copying the arg list*)
-    fun copyargs [] = Seq.cons( ([],ed), Seq.empty)
+    fun copyargs [] = Seq.cons ([],ed) Seq.empty
       | copyargs (uarg::uargs) = Seq.maps (copycons uarg) (copyargs uargs);
     val (uhead,uargs) = strip_comb u;
     val base = body_type env (fastype env (rbinder,uhead));
@@ -577,7 +577,7 @@
   in add_unify 1 ((env, dps), Seq.empty) end;
 
 fun unifiers (params as (thy, env, tus)) =
-  Seq.cons ((fold (Pattern.unify thy) tus env, []), Seq.empty)
+  Seq.cons (fold (Pattern.unify thy) tus env, []) Seq.empty
     handle Pattern.Unif => Seq.empty
          | Pattern.Pattern => hounifiers params;