# HG changeset patch
# User wenzelm
# Date 1142939895 -3600
# Node ID 5c16895d548b5c16ed4c2ec6957cc2974cf941f4
# Parent  15f001295a7ba24be67fe93c8f98724645f5b9b5
avoid polymorphic equality;

diff -r 15f001295a7b -r 5c16895d548b src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/General/name_space.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -68,7 +68,7 @@
 val is_hidden = String.isPrefix "??."
 
 val separator = ".";
-val is_qualified = exists_string (equal separator);
+val is_qualified = exists_string (fn s => s = separator);
 
 val pack = space_implode separator;
 val unpack = space_explode separator;
@@ -229,7 +229,7 @@
     error ("Attempt to declare hidden name " ^ quote name)
   else
     let val names = unpack name in
-      conditional (null names orelse exists (equal "") names) (fn () =>
+      conditional (null names orelse exists (fn s => s = "") names) (fn () =>
         error ("Bad name declaration " ^ quote name));
       fold (add_name name) (map pack (accs names)) space
     end;
diff -r 15f001295a7b -r 5c16895d548b src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/General/path.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -118,7 +118,7 @@
         "$" :: cs => variable_elem cs
       | cs => basic_elem cs);
 
-val unpack_elems = map unpack_elem o filter_out (equal "" orf equal ".");
+val unpack_elems = map unpack_elem o filter_out (fn c => c = "" orelse c = ".");
 
 fun unpack str = Path (norm
   (case space_explode "/" str of
@@ -140,7 +140,7 @@
   | ext e path = split_path (fn (prfx, s) => append (Path prfx) (basic (s ^ "." ^ e))) path;
 
 val split_ext = split_path (fn (prfx, s) => apfst (append (Path prfx))
-  (case take_suffix (not_equal ".") (explode s) of
+  (case take_suffix (fn c => c <> ".") (explode s) of
     ([], _) => (Path [Basic s], "")
   | (cs, e) => (Path [Basic (implode (Library.take (length cs - 1, cs)))], implode e)));
 
diff -r 15f001295a7b -r 5c16895d548b src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/General/symbol.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -414,7 +414,7 @@
 (* source *)
 
 val recover =
-  Scan.any ((not o is_blank) andf not_equal "\"" andf not_eof) >> K [malformed];
+  Scan.any (fn s => not (is_blank s) andalso s <> "\"" andalso not_eof s) >> K [malformed];
 
 fun source do_recover src =
   Source.source stopper (Scan.bulk scan) (if do_recover then SOME recover else NONE) src;
@@ -433,7 +433,7 @@
     else the (Scan.read stopper (Scan.repeat scan) chs)
   end;
 
-val chars_only = not o exists_string (equal "\\");
+val chars_only = not o exists_string (fn s => s = "\\");
 
 
 (* escape *)
diff -r 15f001295a7b -r 5c16895d548b src/Pure/General/url.ML
--- a/src/Pure/General/url.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/General/url.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -53,7 +53,7 @@
 local
 
 val scan_host =
-  (Scan.any1 (not_equal "/" andf Symbol.not_eof) >> implode) --|
+  (Scan.any1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
   Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
 
 val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
diff -r 15f001295a7b -r 5c16895d548b src/Pure/Isar/antiquote.ML
--- a/src/Pure/Isar/antiquote.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/Isar/antiquote.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -36,8 +36,8 @@
 
 val scan_txt =
   T.scan_blank ||
-  T.keep_line ($$ "@" --| Scan.ahead (Scan.one (not_equal "{"))) ||
-  T.keep_line (Scan.one (not_equal "@" andf Symbol.not_sync andf Symbol.not_eof));
+  T.keep_line ($$ "@" --| Scan.ahead (~$$ "{")) ||
+  T.keep_line (Scan.one (fn s => s <> "@" andalso Symbol.not_sync s andalso Symbol.not_eof s));
 
 fun escape "\\" = "\\\\"
   | escape "\"" = "\\\""
@@ -48,7 +48,7 @@
 val scan_ant =
   T.scan_blank ||
   T.scan_string >> quote_escape ||
-  T.keep_line (Scan.one (not_equal "}" andf Symbol.not_sync andf Symbol.not_eof));
+  T.keep_line (Scan.one (fn s => s <> "}" andalso Symbol.not_sync s andalso Symbol.not_eof s));
 
 val scan_antiq =
   T.keep_line ($$ "@" -- $$ "{") |--
diff -r 15f001295a7b -r 5c16895d548b src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/Isar/element.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -342,7 +342,7 @@
 
     val vars = Term.add_vars raw_prop [];
     val frees = ProofContext.rename_frees ctxt [raw_prop] (map (apfst fst) vars);
-    val fixes = rev (filter_out (equal AutoBind.thesisN o #1) frees);
+    val fixes = rev (filter_out (fn (x, _) => x = AutoBind.thesisN) frees);
 
     val prop = Term.instantiate ([], vars ~~ map Free frees) raw_prop;
     val (prems, concl) = Logic.strip_horn prop;
diff -r 15f001295a7b -r 5c16895d548b src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/Isar/outer_lex.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -214,8 +214,8 @@
   scan_blank ||
   keep_line ($$ "\\") |-- !!! "bad escape character in string"
       (scan_blank || keep_line ($$ q || $$ "\\")) ||
-  keep_line (Scan.one (not_equal q andf not_equal "\\" andf
-    Symbol.not_sync andf Symbol.not_eof));
+  keep_line (Scan.one (fn s => s <> q andalso s <> "\\" andalso
+    Symbol.not_sync s andalso Symbol.not_eof s));
 
 fun scan_strs q =
   keep_line ($$ q) |--
@@ -234,8 +234,8 @@
 
 val scan_verb =
   scan_blank ||
-  keep_line ($$ "*" --| Scan.ahead (Scan.one (not_equal "}"))) ||
-  keep_line (Scan.one (not_equal "*" andf Symbol.not_sync andf Symbol.not_eof));
+  keep_line ($$ "*" --| Scan.ahead (~$$ "}")) ||
+  keep_line (Scan.one (fn s => s <> "*" andalso Symbol.not_sync s andalso Symbol.not_eof s));
 
 val scan_verbatim =
   keep_line ($$ "{" -- $$ "*") |--
@@ -245,7 +245,7 @@
 
 (* scan space *)
 
-val is_space = Symbol.is_blank andf not_equal "\n";
+fun is_space s = Symbol.is_blank s andalso s <> "\n";
 
 val scan_space =
   (keep_line (Scan.any1 is_space) -- Scan.optional (incr_line ($$ "\n")) "" ||
@@ -258,8 +258,9 @@
   Scan.lift scan_blank ||
   Scan.depend (fn d => keep_line ($$ "(" ^^ $$ "*") >> pair (d + 1)) ||
   Scan.depend (fn 0 => Scan.fail | d => keep_line ($$ "*" ^^ $$ ")") >> pair (d - 1)) ||
-  Scan.lift (keep_line ($$ "*" --| Scan.ahead (Scan.one (not_equal ")")))) ||
-  Scan.lift (keep_line (Scan.one (not_equal "*" andf Symbol.not_sync andf Symbol.not_eof)));
+  Scan.lift (keep_line ($$ "*" --| Scan.ahead (~$$ ")"))) ||
+  Scan.lift (keep_line (Scan.one (fn s =>
+    s <> "*" andalso Symbol.not_sync s andalso Symbol.not_eof s)));
 
 val scan_comment =
   keep_line ($$ "(" -- $$ "*") |--
diff -r 15f001295a7b -r 5c16895d548b src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/Proof/extraction.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -84,7 +84,7 @@
 
 fun merge_rules
   ({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) =
-  foldr add_rule {next = next, rs = rs1, net = net} (rs2 \\ rs1);
+  foldr add_rule {next = next, rs = rs1, net = net} (subtract (op =) rs1 rs2);
 
 fun condrew thy rules procs =
   let
@@ -205,7 +205,7 @@
     {realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
      typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
      types = merge_alists types1 types2,
-     realizers = Symtab.merge_list (eq_set o pairself #1) (realizers1, realizers2),
+     realizers = Symtab.merge_list (gen_eq_set (op =) o pairself #1) (realizers1, realizers2),
      defs = gen_merge_lists eq_thm defs1 defs2,
      expand = merge_lists expand1 expand2,
      prep = (case prep1 of NONE => prep2 | _ => prep1)};
@@ -483,7 +483,7 @@
 
       in foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
 
-    fun find vs = Option.map snd o find_first (curry eq_set vs o fst);
+    fun find vs = Option.map snd o find_first (curry (gen_eq_set (op =)) vs o fst);
     fun find' s = map snd o List.filter (equal s o fst)
 
     fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw
diff -r 15f001295a7b -r 5c16895d548b src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -111,7 +111,7 @@
       | rename (prf' as PThm ((s, tags), prf, prop, Ts)) =
           let
             val prop' = if_none (AList.lookup (op =) thms' s) (Bound 0);
-            val ps = map fst (the (Symtab.lookup thms s)) \ prop'
+            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),
               prf, prop, Ts)
@@ -248,7 +248,8 @@
 
 fun proof_syntax prf =
   let
-    val thm_names = map fst (Symtab.dest (thms_of_proof prf Symtab.empty)) \ "";
+    val thm_names = filter_out (equal "")
+      (map fst (Symtab.dest (thms_of_proof prf Symtab.empty)));
     val axm_names = map fst (Symtab.dest (axms_of_proof prf Symtab.empty));
   in
     add_proof_syntax #>
diff -r 15f001295a7b -r 5c16895d548b src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/Proof/reconstruct.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -246,7 +246,7 @@
       (Vartab.foldl (add_term_ixns o apsnd (snd o snd)) ([], asol), iTs);
     fun check_cs [] = []
       | check_cs ((u, p, vs)::ps) =
-          let val vs' = vs \\ dom;
+          let val vs' = subtract (op =) dom vs;
           in if vs = vs' then (u, p, vs)::check_cs ps
              else (true, p, vs' union vran)::check_cs ps
           end
diff -r 15f001295a7b -r 5c16895d548b src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -222,8 +222,8 @@
 
 val scan_chr =
   $$ "\\" |-- Scan.one Symbol.not_eof ||
-  Scan.one (not_equal "'" andf Symbol.not_eof) ||
-  $$ "'" --| Scan.ahead (Scan.one (not_equal "'"));
+  Scan.one (fn s => s <> "'" andalso Symbol.not_eof s) ||
+  $$ "'" --| Scan.ahead (~$$ "'");
 
 val scan_str =
   $$ "'" |-- $$ "'" |-- !! (lex_err "missing end of string" "''")
@@ -243,8 +243,8 @@
 val scan_cmt =
   Scan.depend (fn d => $$ "(" ^^ $$ "*" >> pair (d + 1)) ||
   Scan.depend (fn 0 => Scan.fail | d => $$ "*" ^^ $$ ")" >> pair (d - 1)) ||
-  Scan.lift ($$ "*" --| Scan.ahead (Scan.one (not_equal ")"))) ||
-  Scan.lift (Scan.one (not_equal "*" andf Symbol.not_eof));
+  Scan.lift ($$ "*" --| Scan.ahead (~$$ ")")) ||
+  Scan.lift (Scan.one (fn s => s <> "*" andalso Symbol.not_eof s));
 
 val scan_comment =
   $$ "(" -- $$ "*" -- !! (lex_err "missing end of comment" "(*")
diff -r 15f001295a7b -r 5c16895d548b src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/Syntax/parser.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -60,7 +60,7 @@
    (used for expanding chain list)*)
 fun connected_with _ [] relatives = relatives
   | connected_with chains (root :: roots) relatives =
-    let val branches = these (AList.lookup (op =) chains root) \\ relatives;
+    let val branches = subtract (op =) relatives (these (AList.lookup (op =) chains root));
     in connected_with chains (branches @ roots) (branches @ relatives) end;
 
 (* convert productions to grammar;
@@ -93,7 +93,7 @@
                 let
                   val ((to_nts, to_tks), ps) = Array.sub (prods, to);
 
-                  val new_tks = from_tks \\ to_tks;  (*added lookahead tokens*)
+                  val new_tks = subtract (op =) to_tks from_tks;  (*added lookahead tokens*)
                 in Array.update (prods, to, ((to_nts, to_tks @ new_tks), ps));
                    copy_lookahead tos (if null new_tks then added
                                        else (to, new_tks) :: added)
@@ -149,9 +149,9 @@
                       let
                         val new_lambda = is_none tk andalso nts subset lambdas;
 
-                        val new_tks = (if is_some tk then [the tk] else []) @
-                          Library.foldl token_union ([], map starts_for_nt nts) \\
-                          l_starts;
+                        val new_tks = subtract (op =) l_starts
+                          ((if is_some tk then [the tk] else []) @
+                            Library.foldl token_union ([], map starts_for_nt nts));
 
                         val added_tks' = token_union (new_tks, added_tks);
 
@@ -199,7 +199,7 @@
                       val (add_lambda, nt_dependencies, added_tks, nt_prods') =
                         examine_prods tk_prods false [] [] nt_prods;
 
-                      val added_nts = nt_dependencies \\ old_nts;
+                      val added_nts = subtract (op =) old_nts nt_dependencies;
 
                       val added_lambdas' =
                         if add_lambda then nt :: added_lambdas
@@ -222,11 +222,11 @@
                 val (added_lambdas, added_starts') =
                   process_nts dependent [] added_starts;
 
-                val added_lambdas' = added_lambdas \\ lambdas;
+                val added_lambdas' = subtract (op =) lambdas added_lambdas;
               in propagate_lambda (ls @ added_lambdas') added_starts'
                                   (added_lambdas' @ lambdas)
               end;
-        in propagate_lambda (lambdas' \\ lambdas) added_starts lambdas' end;
+        in propagate_lambda (subtract (op =) lambdas lambdas') added_starts lambdas' end;
 
       (*insert production into grammar*)
       val (added_starts', prod_count') =
@@ -748,8 +748,7 @@
             val dummy =
               if not (!warned) andalso
                  length (new_states @ States) > (!branching_level) then
-                (warning "Currently parsed expression could be \
-                         \extremely ambiguous.";
+                (warning "Currently parsed expression could be extremely ambiguous.";
                  warned := true)
               else ();
           in
diff -r 15f001295a7b -r 5c16895d548b src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -217,7 +217,7 @@
   scan_sym >> SOME ||
   $$ "'" -- Scan.one Symbol.is_blank >> K NONE;
 
-val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (Scan.one (not_equal "'"));
+val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'");
 val read_symbs = List.mapPartial I o the o Scan.read Symbol.stopper scan_symbs;
 
 fun unique_index xsymbs =
diff -r 15f001295a7b -r 5c16895d548b src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -140,14 +140,14 @@
 val no_bracketsN = "no_brackets";
 
 fun no_brackets () =
-  find_first (equal bracketsN orf equal no_bracketsN) (! print_mode)
+  find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN) (! print_mode)
     = SOME no_bracketsN;
 
 val type_bracketsN = "type_brackets";
 val no_type_bracketsN = "no_type_brackets";
 
 fun no_type_brackets () =
-  Library.find_first (equal type_bracketsN orf equal no_type_bracketsN) (! print_mode)
+  find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN) (! print_mode)
     <> SOME type_bracketsN;
 
 
diff -r 15f001295a7b -r 5c16895d548b src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/Thy/html.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -223,7 +223,7 @@
 in
 
 fun output_width str =
-  if not (exists_string (equal "\\" orf equal "<" orf equal ">" orf equal "&") str)
+  if not (exists_string (fn s => s = "\\" orelse s = "<" orelse s = ">" orelse s = "&") str)
   then Symbol.default_output str
   else
     let val (syms, width) = fold_map (fn (w, s) => fn width => (s, w + width))
diff -r 15f001295a7b -r 5c16895d548b src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/Thy/present.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -261,7 +261,7 @@
 fun update_index dir name =
   (case try get_entries dir of
     NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.pack dir))
-  | SOME es => (put_entries ((es \ name) @ [name]) dir; create_index dir));
+  | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir));
 
 
 (* document versions *)
diff -r 15f001295a7b -r 5c16895d548b src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/Thy/thy_info.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -171,8 +171,8 @@
 fun relevant_names names =
   let
     val (finished, unfinished) =
-      List.filter (equal Context.draftN orf known_thy) names
-      |> List.partition (not_equal Context.draftN andf is_finished);
+      List.filter (fn name => name = Context.draftN orelse known_thy name) names
+      |> List.partition (fn name => name <> Context.draftN andalso is_finished name);
   in (if not (null finished) then [List.last finished] else []) @ unfinished end;
 
 in
diff -r 15f001295a7b -r 5c16895d548b src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/pure_thy.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -107,7 +107,7 @@
   Thm.put_name_tags (Thm.name_of_thm thm, f (#2 (Thm.get_name_tags thm))) thm;
 
 fun tag_rule tg = map_tags (fn tgs => if tg mem tgs then tgs else tgs @ [tg]);
-fun untag_rule s = map_tags (filter_out (equal s o #1));
+fun untag_rule s = map_tags (filter_out (fn (s', _) => s = s'));
 
 fun tag tg x = Thm.rule_attribute (K (tag_rule tg)) x;
 fun untag s x = Thm.rule_attribute (K (untag_rule s)) x;
diff -r 15f001295a7b -r 5c16895d548b src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/thm.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -450,7 +450,7 @@
 val concl_of = Logic.strip_imp_concl o prop_of;
 val prems_of = Logic.strip_imp_prems o prop_of;
 fun nprems_of th = Logic.count_prems (prop_of th, 0);
-val no_prems = equal 0 o nprems_of;
+fun no_prems th = nprems_of th = 0;
 
 fun major_prem_of th =
   (case prems_of th of
diff -r 15f001295a7b -r 5c16895d548b src/Pure/type.ML
--- a/src/Pure/type.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/type.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -220,7 +220,8 @@
 
 fun varify (t, fixed) =
   let
-    val fs = add_term_tfrees (t, []) \\ fixed;
+    val fs = Term.fold_types (Term.fold_atyps
+      (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
     val ixns = add_term_tvar_ixns (t, []);
     val fmap = fs ~~ map (rpair 0) (variantlist (map fst fs, map #1 ixns))
     fun thaw (f as (a, S)) =