--- 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;
--- 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)));
--- 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 *)
--- 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);
--- 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 ($$ "@" -- $$ "{") |--
--- 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;
--- 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 ($$ "(" -- $$ "*") |--
--- 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
--- 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 #>
--- 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
--- 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" "(*")
--- 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
--- 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 =
--- 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;
--- 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))
--- 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 *)
--- 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
--- 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;
--- 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
--- 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)) =