--- 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 *)
--- 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'
--- 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,
--- 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
--- 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
--- 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;
--- 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
--- 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),
--- 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
--- 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 *)
--- 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.$$$ ")") "" --
--- 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;
--- 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 =