# HG changeset patch
# User wenzelm
# Date 1222448876 -7200
# Node ID c879d88d038a497ee27317d3f2065fa7224f5f37
# Parent  27f1b5cc5f9bcd162d477d9e4a5f80ac43906847
eliminated polymorphic equality;

diff -r 27f1b5cc5f9b -r c879d88d038a src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Sep 26 17:24:15 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Sep 26 19:07:56 2008 +0200
@@ -249,7 +249,7 @@
 val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof;
 val global_done_proof = Toplevel.end_proof (K Proof.global_done_proof);
 
-val skip_global_qed = Toplevel.skip_proof_to_theory (equal 1);
+val skip_global_qed = Toplevel.skip_proof_to_theory (fn n => n = 1);
 
 
 (* common endings *)
diff -r 27f1b5cc5f9b -r c879d88d038a src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Sep 26 17:24:15 2008 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Sep 26 19:07:56 2008 +0200
@@ -592,7 +592,7 @@
       [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
     val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
     val err_msg =
-      if forall (equal "" o #1) ids then msg
+      if forall (fn (s, _) => s = "") ids then msg
       else msg ^ "\n" ^ Pretty.string_of (Pretty.block
         (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
   in error err_msg end;
@@ -1168,7 +1168,7 @@
     val th = abstract_thm (ProofContext.theory_of ctxt) eq;
     fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
   in
-    exists (equal y o #1) xs andalso
+    exists (fn (x, _) => x = y) xs andalso
       err "Attempt to define previously specified variable";
     exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
       err "Attempt to redefine variable";
@@ -1988,7 +1988,7 @@
     val export = Thm.close_derivation o Goal.norm_result o
       singleton (ProofContext.export view_ctxt thy_ctxt);
     val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
-    val elems' = maps #2 (filter (equal "" o #1 o #1) elemss''');
+    val elems' = maps #2 (filter (fn ((s, _), _) => s = "") elemss''');
     val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
     val axs' = map (Element.assume_witness thy') stmt';
     val loc_ctxt = thy'
diff -r 27f1b5cc5f9b -r c879d88d038a src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Sep 26 17:24:15 2008 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Sep 26 19:07:56 2008 +0200
@@ -342,7 +342,7 @@
       | subgoals n = string_of_int n ^ " subgoals";
 
     fun description strs =
-      (case filter_out (equal "") strs of [] => ""
+      (case filter_out (fn s => s = "") strs of [] => ""
       | strs' => enclose " (" ")" (commas strs'));
 
     fun prt_goal (SOME (ctxt, (i,
diff -r 27f1b5cc5f9b -r c879d88d038a src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Sep 26 17:24:15 2008 +0200
+++ b/src/Pure/Proof/extraction.ML	Fri Sep 26 19:07:56 2008 +0200
@@ -70,7 +70,7 @@
   | rlz_proc _ = NONE;
 
 val unpack_ixn = apfst implode o apsnd (fst o read_int o tl) o
-  take_prefix (not o equal ":") o explode;
+  take_prefix (fn s => s <> ":") o explode;
 
 type rules =
   {next: int, rs: ((term * term) list * (term * term)) list,
@@ -259,7 +259,7 @@
 val add_typeof_eqns = gen_add_typeof_eqns read_condeq;
 
 fun thaw (T as TFree (a, S)) =
-      if exists_string (equal ":") a then TVar (unpack_ixn a, S) else T
+      if exists_string (fn s => s = ":") a then TVar (unpack_ixn a, S) else T
   | thaw (Type (a, Ts)) = Type (a, map thaw Ts)
   | thaw T = T;
 
@@ -473,7 +473,7 @@
       in List.foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
 
     fun find (vs: string list) = 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 find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
 
     fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw
       (condrew thy' rrews (procs @ [typroc vs, rlz_proc])) (list_abs
diff -r 27f1b5cc5f9b -r c879d88d038a src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Fri Sep 26 17:24:15 2008 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Sep 26 19:07:56 2008 +0200
@@ -217,7 +217,7 @@
 fun cterm_of_proof thy prf =
   let
     val (prf', tab) = disambiguate_names thy prf;
-    val thm_names = filter_out (equal "")
+    val thm_names = filter_out (fn s => s = "")
       (map fst (PureThy.all_thms_of thy) @ map fst (Symtab.dest tab));
     val axm_names = map fst (Theory.all_axioms_of thy);
     val thy' = thy
@@ -231,7 +231,7 @@
 
 fun read_term thy =
   let
-    val thm_names = filter_out (equal "") (map fst (PureThy.all_thms_of thy));
+    val thm_names = filter_out (fn s => s = "") (map fst (PureThy.all_thms_of thy));
     val axm_names = map fst (Theory.all_axioms_of thy);
     val ctxt = thy
       |> add_proof_syntax
@@ -252,7 +252,7 @@
 
 fun proof_syntax prf =
   let
-    val thm_names = filter_out (equal "")
+    val thm_names = filter_out (fn s => s = "")
       (map fst (Symtab.dest (thms_of_proof prf Symtab.empty)));
     val axm_names = map fst (Symtab.dest (axms_of_proof prf Symtab.empty));
   in
diff -r 27f1b5cc5f9b -r c879d88d038a src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Sep 26 17:24:15 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Sep 26 19:07:56 2008 +0200
@@ -41,7 +41,7 @@
   | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
 
 fun xsymbols_output s =
-  if print_mode_active Symbol.xsymbolsN andalso exists_string (equal "\\") s then
+  if print_mode_active Symbol.xsymbolsN andalso exists_string (fn c => c = "\\") s then
     let val syms = Symbol.explode s
     in (implode (map xsym_output syms), Symbol.length syms) end
   else Output.default_output s;
diff -r 27f1b5cc5f9b -r c879d88d038a src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Sep 26 17:24:15 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Sep 26 19:07:56 2008 +0200
@@ -613,7 +613,7 @@
                 val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *)
                 val thy = Context.theory_of_proof ctx
                 val ths = [PureThy.get_thm thy thmname]
-                val deps = filter_out (equal "")
+                val deps = filter_out (fn s => s = "")
                                       (Symtab.keys (fold Proofterm.thms_of_proof
                                                          (map Thm.proof_of ths) Symtab.empty))
             in
diff -r 27f1b5cc5f9b -r c879d88d038a src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Sep 26 17:24:15 2008 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Sep 26 19:07:56 2008 +0200
@@ -405,7 +405,7 @@
 fun pretty_gram (Syntax (tabs, _)) =
   let
     val {lexicon, prmodes, gram, prtabs, ...} = tabs;
-    val prmodes' = sort_strings (filter_out (equal "") prmodes);
+    val prmodes' = sort_strings (filter_out (fn s => s = "") prmodes);
   in
     [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon),
       Pretty.big_list "prods:" (Parser.pretty_gram gram),
diff -r 27f1b5cc5f9b -r c879d88d038a src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Fri Sep 26 17:24:15 2008 +0200
+++ b/src/Pure/Thy/latex.ML	Fri Sep 26 19:07:56 2008 +0200
@@ -102,7 +102,7 @@
 
 structure T = OuterLex;
 
-val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
+val invisible_token = T.keyword_with (fn s => s = ";") orf T.is_kind T.Comment;
 
 fun output_basic tok =
   let val s = T.content_of tok in
diff -r 27f1b5cc5f9b -r c879d88d038a src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Fri Sep 26 17:24:15 2008 +0200
+++ b/src/Pure/Thy/present.ML	Fri Sep 26 19:07:56 2008 +0200
@@ -273,7 +273,7 @@
 
 fun read_versions strs =
   rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_version strs)))
-  |> filter_out (equal "-" o #2);
+  |> filter_out (fn (_, s) => s = "-");
 
 
 (* init session *)
diff -r 27f1b5cc5f9b -r c879d88d038a src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Fri Sep 26 17:24:15 2008 +0200
+++ b/src/Pure/codegen.ML	Fri Sep 26 19:07:56 2008 +0200
@@ -341,7 +341,7 @@
     fun prep thy = map (fn th =>
       let val prop = prop_of th
       in
-        if forall (fn name => exists_Const (equal name o fst) prop) names
+        if forall (fn name => exists_Const (fn (c, _) => c = name) prop) names
         then rewrite_rule [eqn'] (Thm.transfer thy th)
         else th
       end)
@@ -400,7 +400,7 @@
 fun is_ascii_letdig x = Symbol.is_ascii_letter x orelse
   Symbol.is_ascii_digit x orelse Symbol.is_ascii_quasi x;
 
-fun dest_sym s = (case split_last (snd (take_prefix (equal "\\") (explode s))) of
+fun dest_sym s = (case split_last (snd (take_prefix (fn c => c = "\\") (explode s))) of
     ("<" :: "^" :: xs, ">") => (true, implode xs)
   | ("<" :: xs, ">") => (false, implode xs)
   | _ => sys_error "dest_sym");
@@ -802,7 +802,7 @@
     fun string_of_cycle (a :: b :: cs) =
           let val SOME (x, y) = get_first (fn (x, (_, a', _)) =>
             if a = a' then Option.map (pair x)
-              (find_first (equal b o #2 o Graph.get_node gr)
+              (find_first ((fn (_, b', _) => b' = b) o Graph.get_node gr)
                 (Graph.imm_succs gr x))
             else NONE) code
           in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end
@@ -813,7 +813,7 @@
         val modules = distinct (op =) (map (#2 o snd) code);
         val mod_gr = fold_rev Graph.add_edge_acyclic
           (maps (fn (s, (_, module, _)) => map (pair module)
-            (filter_out (equal module) (map (#2 o Graph.get_node gr)
+            (filter_out (fn s => s = module) (map (#2 o Graph.get_node gr)
               (Graph.imm_succs gr s)))) code)
           (fold_rev (Graph.new_node o rpair ()) modules Graph.empty);
         val modules' =
@@ -830,7 +830,7 @@
 fun gen_generate_code prep_term thy modules module xs =
   let
     val _ = (module <> "" orelse
-        member (op =) (!mode) "library" andalso forall (equal "" o fst) xs)
+        member (op =) (!mode) "library" andalso forall (fn (s, _) => s = "") xs)
       orelse error "missing module name";
     val graphs = get_modules thy;
     val defs = mk_deftab thy;
@@ -1012,8 +1012,8 @@
 
 val _ = List.app OuterKeyword.keyword ["attach", "file", "contains"];
 
-fun strip_whitespace s = implode (fst (take_suffix (equal "\n" orf equal " ")
-  (snd (take_prefix (equal "\n" orf equal " ") (explode s))))) ^ "\n";
+fun strip_whitespace s = implode (fst (take_suffix (fn c => c = "\n" orelse c = " ")
+  (snd (take_prefix (fn c => c = "\n" orelse c = " ") (explode s))))) ^ "\n";
 
 val parse_attach = Scan.repeat (P.$$$ "attach" |--
   Scan.optional (P.$$$ "(" |-- P.xname --| P.$$$ ")") "" --
diff -r 27f1b5cc5f9b -r c879d88d038a src/Pure/context.ML
--- a/src/Pure/context.ML	Fri Sep 26 17:24:15 2008 +0200
+++ b/src/Pure/context.ML	Fri Sep 26 19:07:56 2008 +0200
@@ -210,8 +210,8 @@
 fun exists_name name (thy as Theory ({id, ids, iids, ...}, _, _, _)) =
   name = theory_name thy orelse
   name = #2 id orelse
-  Inttab.exists (equal name o #2) ids orelse
-  Inttab.exists (equal name o #2) iids;
+  Inttab.exists (fn (_, a) => a = name) ids orelse
+  Inttab.exists (fn (_, a) => a = name) iids;
 
 fun names_of (Theory ({id, ids, ...}, _, _, _)) =
   rev (#2 id :: Inttab.fold (cons o #2) ids []);
@@ -255,7 +255,7 @@
 
 fun check_ins id ids =
   if draft_id id orelse Inttab.defined ids (#1 id) then ids
-  else if Inttab.exists (equal (#2 id) o #2) ids then
+  else if Inttab.exists (fn (_, a) => a = #2 id) ids then
     error ("Different versions of theory component " ^ quote (#2 id))
   else Inttab.update id ids;
 
@@ -275,8 +275,7 @@
 
 val eq_thy = eq_id o pairself (#id o identity_of);
 
-fun proper_subthy
-    (Theory ({id = (i, _), ...}, _, _, _), Theory ({ids, iids, ...}, _, _, _)) =
+fun proper_subthy (Theory ({id = (i, _), ...}, _, _, _), Theory ({ids, iids, ...}, _, _, _)) =
   Inttab.defined ids i orelse Inttab.defined iids i;
 
 fun subthy thys = eq_thy thys orelse proper_subthy thys;
diff -r 27f1b5cc5f9b -r c879d88d038a src/Tools/induct.ML
--- a/src/Tools/induct.ML	Fri Sep 26 17:24:15 2008 +0200
+++ b/src/Tools/induct.ML	Fri Sep 26 19:07:56 2008 +0200
@@ -478,7 +478,7 @@
           let
             val xs = rename_params (Logic.strip_params A);
             val xs' =
-              (case List.filter (equal x) xs of
+              (case filter (fn x' => x' = x) xs of
                 [] => xs | [_] => xs | _ => index 1 xs);
           in Logic.list_rename_params (xs', A) end;
         fun rename_prop p =