1.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Sep 26 17:24:15 2008 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Sep 26 19:07:56 2008 +0200
     1.3 @@ -249,7 +249,7 @@
     1.4  val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof;
     1.5  val global_done_proof = Toplevel.end_proof (K Proof.global_done_proof);
     1.6  
     1.7 -val skip_global_qed = Toplevel.skip_proof_to_theory (equal 1);
     1.8 +val skip_global_qed = Toplevel.skip_proof_to_theory (fn n => n = 1);
     1.9  
    1.10  
    1.11  (* common endings *)

     2.1 --- a/src/Pure/Isar/locale.ML	Fri Sep 26 17:24:15 2008 +0200
     2.2 +++ b/src/Pure/Isar/locale.ML	Fri Sep 26 19:07:56 2008 +0200
     2.3 @@ -592,7 +592,7 @@
     2.4        [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
     2.5      val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
     2.6      val err_msg =
     2.7 -      if forall (equal "" o #1) ids then msg
     2.8 +      if forall (fn (s, _) => s = "") ids then msg
     2.9        else msg ^ "\n" ^ Pretty.string_of (Pretty.block
    2.10          (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
    2.11    in error err_msg end;
    2.12 @@ -1168,7 +1168,7 @@
    2.13      val th = abstract_thm (ProofContext.theory_of ctxt) eq;
    2.14      fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
    2.15    in
    2.16 -    exists (equal y o #1) xs andalso
    2.17 +    exists (fn (x, _) => x = y) xs andalso
    2.18        err "Attempt to define previously specified variable";
    2.19      exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
    2.20        err "Attempt to redefine variable";
    2.21 @@ -1988,7 +1988,7 @@
    2.22      val export = Thm.close_derivation o Goal.norm_result o
    2.23        singleton (ProofContext.export view_ctxt thy_ctxt);
    2.24      val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
    2.25 -    val elems' = maps #2 (filter (equal "" o #1 o #1) elemss''');
    2.26 +    val elems' = maps #2 (filter (fn ((s, _), _) => s = "") elemss''');
    2.27      val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
    2.28      val axs' = map (Element.assume_witness thy') stmt';
    2.29      val loc_ctxt = thy'

     3.1 --- a/src/Pure/Isar/proof.ML	Fri Sep 26 17:24:15 2008 +0200
     3.2 +++ b/src/Pure/Isar/proof.ML	Fri Sep 26 19:07:56 2008 +0200
     3.3 @@ -342,7 +342,7 @@
     3.4        | subgoals n = string_of_int n ^ " subgoals";
     3.5  
     3.6      fun description strs =
     3.7 -      (case filter_out (equal "") strs of [] => ""
     3.8 +      (case filter_out (fn s => s = "") strs of [] => ""
     3.9        | strs' => enclose " (" ")" (commas strs'));
    3.10  
    3.11      fun prt_goal (SOME (ctxt, (i,

     4.1 --- a/src/Pure/Proof/extraction.ML	Fri Sep 26 17:24:15 2008 +0200
     4.2 +++ b/src/Pure/Proof/extraction.ML	Fri Sep 26 19:07:56 2008 +0200
     4.3 @@ -70,7 +70,7 @@
     4.4    | rlz_proc _ = NONE;
     4.5  
     4.6  val unpack_ixn = apfst implode o apsnd (fst o read_int o tl) o
     4.7 -  take_prefix (not o equal ":") o explode;
     4.8 +  take_prefix (fn s => s <> ":") o explode;
     4.9  
    4.10  type rules =
    4.11    {next: int, rs: ((term * term) list * (term * term)) list,
    4.12 @@ -259,7 +259,7 @@
    4.13  val add_typeof_eqns = gen_add_typeof_eqns read_condeq;
    4.14  
    4.15  fun thaw (T as TFree (a, S)) =
    4.16 -      if exists_string (equal ":") a then TVar (unpack_ixn a, S) else T
    4.17 +      if exists_string (fn s => s = ":") a then TVar (unpack_ixn a, S) else T
    4.18    | thaw (Type (a, Ts)) = Type (a, map thaw Ts)
    4.19    | thaw T = T;
    4.20  
    4.21 @@ -473,7 +473,7 @@
    4.22        in List.foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
    4.23  
    4.24      fun find (vs: string list) = Option.map snd o find_first (curry (gen_eq_set (op =)) vs o fst);
    4.25 -    fun find' s = map snd o List.filter (equal s o fst)
    4.26 +    fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
    4.27  
    4.28      fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw
    4.29        (condrew thy' rrews (procs @ [typroc vs, rlz_proc])) (list_abs

     5.1 --- a/src/Pure/Proof/proof_syntax.ML	Fri Sep 26 17:24:15 2008 +0200
     5.2 +++ b/src/Pure/Proof/proof_syntax.ML	Fri Sep 26 19:07:56 2008 +0200
     5.3 @@ -217,7 +217,7 @@
     5.4  fun cterm_of_proof thy prf =
     5.5    let
     5.6      val (prf', tab) = disambiguate_names thy prf;
     5.7 -    val thm_names = filter_out (equal "")
     5.8 +    val thm_names = filter_out (fn s => s = "")
     5.9        (map fst (PureThy.all_thms_of thy) @ map fst (Symtab.dest tab));
    5.10      val axm_names = map fst (Theory.all_axioms_of thy);
    5.11      val thy' = thy
    5.12 @@ -231,7 +231,7 @@
    5.13  
    5.14  fun read_term thy =
    5.15    let
    5.16 -    val thm_names = filter_out (equal "") (map fst (PureThy.all_thms_of thy));
    5.17 +    val thm_names = filter_out (fn s => s = "") (map fst (PureThy.all_thms_of thy));
    5.18      val axm_names = map fst (Theory.all_axioms_of thy);
    5.19      val ctxt = thy
    5.20        |> add_proof_syntax
    5.21 @@ -252,7 +252,7 @@
    5.22  
    5.23  fun proof_syntax prf =
    5.24    let
    5.25 -    val thm_names = filter_out (equal "")
    5.26 +    val thm_names = filter_out (fn s => s = "")
    5.27        (map fst (Symtab.dest (thms_of_proof prf Symtab.empty)));
    5.28      val axm_names = map fst (Symtab.dest (axms_of_proof prf Symtab.empty));
    5.29    in

     6.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Sep 26 17:24:15 2008 +0200
     6.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Sep 26 19:07:56 2008 +0200
     6.3 @@ -41,7 +41,7 @@
     6.4    | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
     6.5  
     6.6  fun xsymbols_output s =
     6.7 -  if print_mode_active Symbol.xsymbolsN andalso exists_string (equal "\\") s then
     6.8 +  if print_mode_active Symbol.xsymbolsN andalso exists_string (fn c => c = "\\") s then
     6.9      let val syms = Symbol.explode s
    6.10      in (implode (map xsym_output syms), Symbol.length syms) end
    6.11    else Output.default_output s;

     7.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Sep 26 17:24:15 2008 +0200
     7.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Sep 26 19:07:56 2008 +0200
     7.3 @@ -613,7 +613,7 @@
     7.4                  val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *)
     7.5                  val thy = Context.theory_of_proof ctx
     7.6                  val ths = [PureThy.get_thm thy thmname]
     7.7 -                val deps = filter_out (equal "")
     7.8 +                val deps = filter_out (fn s => s = "")
     7.9                                        (Symtab.keys (fold Proofterm.thms_of_proof
    7.10                                                           (map Thm.proof_of ths) Symtab.empty))
    7.11              in

     8.1 --- a/src/Pure/Syntax/syntax.ML	Fri Sep 26 17:24:15 2008 +0200
     8.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Sep 26 19:07:56 2008 +0200
     8.3 @@ -405,7 +405,7 @@
     8.4  fun pretty_gram (Syntax (tabs, _)) =
     8.5    let
     8.6      val {lexicon, prmodes, gram, prtabs, ...} = tabs;
     8.7 -    val prmodes' = sort_strings (filter_out (equal "") prmodes);
     8.8 +    val prmodes' = sort_strings (filter_out (fn s => s = "") prmodes);
     8.9    in
    8.10      [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon),
    8.11        Pretty.big_list "prods:" (Parser.pretty_gram gram),

     9.1 --- a/src/Pure/Thy/latex.ML	Fri Sep 26 17:24:15 2008 +0200
     9.2 +++ b/src/Pure/Thy/latex.ML	Fri Sep 26 19:07:56 2008 +0200
     9.3 @@ -102,7 +102,7 @@
     9.4  
     9.5  structure T = OuterLex;
     9.6  
     9.7 -val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
     9.8 +val invisible_token = T.keyword_with (fn s => s = ";") orf T.is_kind T.Comment;
     9.9  
    9.10  fun output_basic tok =
    9.11    let val s = T.content_of tok in

    10.1 --- a/src/Pure/Thy/present.ML	Fri Sep 26 17:24:15 2008 +0200
    10.2 +++ b/src/Pure/Thy/present.ML	Fri Sep 26 19:07:56 2008 +0200
    10.3 @@ -273,7 +273,7 @@
    10.4  
    10.5  fun read_versions strs =
    10.6    rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_version strs)))
    10.7 -  |> filter_out (equal "-" o #2);
    10.8 +  |> filter_out (fn (_, s) => s = "-");
    10.9  
   10.10  
   10.11  (* init session *)

    11.1 --- a/src/Pure/codegen.ML	Fri Sep 26 17:24:15 2008 +0200
    11.2 +++ b/src/Pure/codegen.ML	Fri Sep 26 19:07:56 2008 +0200
    11.3 @@ -341,7 +341,7 @@
    11.4      fun prep thy = map (fn th =>
    11.5        let val prop = prop_of th
    11.6        in
    11.7 -        if forall (fn name => exists_Const (equal name o fst) prop) names
    11.8 +        if forall (fn name => exists_Const (fn (c, _) => c = name) prop) names
    11.9          then rewrite_rule [eqn'] (Thm.transfer thy th)
   11.10          else th
   11.11        end)
   11.12 @@ -400,7 +400,7 @@
   11.13  fun is_ascii_letdig x = Symbol.is_ascii_letter x orelse
   11.14    Symbol.is_ascii_digit x orelse Symbol.is_ascii_quasi x;
   11.15  
   11.16 -fun dest_sym s = (case split_last (snd (take_prefix (equal "\\") (explode s))) of
   11.17 +fun dest_sym s = (case split_last (snd (take_prefix (fn c => c = "\\") (explode s))) of
   11.18      ("<" :: "^" :: xs, ">") => (true, implode xs)
   11.19    | ("<" :: xs, ">") => (false, implode xs)
   11.20    | _ => sys_error "dest_sym");
   11.21 @@ -802,7 +802,7 @@
   11.22      fun string_of_cycle (a :: b :: cs) =
   11.23            let val SOME (x, y) = get_first (fn (x, (_, a', _)) =>
   11.24              if a = a' then Option.map (pair x)
   11.25 -              (find_first (equal b o #2 o Graph.get_node gr)
   11.26 +              (find_first ((fn (_, b', _) => b' = b) o Graph.get_node gr)
   11.27                  (Graph.imm_succs gr x))
   11.28              else NONE) code
   11.29            in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end
   11.30 @@ -813,7 +813,7 @@
   11.31          val modules = distinct (op =) (map (#2 o snd) code);
   11.32          val mod_gr = fold_rev Graph.add_edge_acyclic
   11.33            (maps (fn (s, (_, module, _)) => map (pair module)
   11.34 -            (filter_out (equal module) (map (#2 o Graph.get_node gr)
   11.35 +            (filter_out (fn s => s = module) (map (#2 o Graph.get_node gr)
   11.36                (Graph.imm_succs gr s)))) code)
   11.37            (fold_rev (Graph.new_node o rpair ()) modules Graph.empty);
   11.38          val modules' =
   11.39 @@ -830,7 +830,7 @@
   11.40  fun gen_generate_code prep_term thy modules module xs =
   11.41    let
   11.42      val _ = (module <> "" orelse
   11.43 -        member (op =) (!mode) "library" andalso forall (equal "" o fst) xs)
   11.44 +        member (op =) (!mode) "library" andalso forall (fn (s, _) => s = "") xs)
   11.45        orelse error "missing module name";
   11.46      val graphs = get_modules thy;
   11.47      val defs = mk_deftab thy;
   11.48 @@ -1012,8 +1012,8 @@
   11.49  
   11.50  val _ = List.app OuterKeyword.keyword ["attach", "file", "contains"];
   11.51  
   11.52 -fun strip_whitespace s = implode (fst (take_suffix (equal "\n" orf equal " ")
   11.53 -  (snd (take_prefix (equal "\n" orf equal " ") (explode s))))) ^ "\n";
   11.54 +fun strip_whitespace s = implode (fst (take_suffix (fn c => c = "\n" orelse c = " ")
   11.55 +  (snd (take_prefix (fn c => c = "\n" orelse c = " ") (explode s))))) ^ "\n";
   11.56  
   11.57  val parse_attach = Scan.repeat (P.$$$ "attach" |--
   11.58    Scan.optional (P.$$$ "(" |-- P.xname --| P.$$$ ")") "" --

    12.1 --- a/src/Pure/context.ML	Fri Sep 26 17:24:15 2008 +0200
    12.2 +++ b/src/Pure/context.ML	Fri Sep 26 19:07:56 2008 +0200
    12.3 @@ -210,8 +210,8 @@
    12.4  fun exists_name name (thy as Theory ({id, ids, iids, ...}, _, _, _)) =
    12.5    name = theory_name thy orelse
    12.6    name = #2 id orelse
    12.7 -  Inttab.exists (equal name o #2) ids orelse
    12.8 -  Inttab.exists (equal name o #2) iids;
    12.9 +  Inttab.exists (fn (_, a) => a = name) ids orelse
   12.10 +  Inttab.exists (fn (_, a) => a = name) iids;
   12.11  
   12.12  fun names_of (Theory ({id, ids, ...}, _, _, _)) =
   12.13    rev (#2 id :: Inttab.fold (cons o #2) ids []);
   12.14 @@ -255,7 +255,7 @@
   12.15  
   12.16  fun check_ins id ids =
   12.17    if draft_id id orelse Inttab.defined ids (#1 id) then ids
   12.18 -  else if Inttab.exists (equal (#2 id) o #2) ids then
   12.19 +  else if Inttab.exists (fn (_, a) => a = #2 id) ids then
   12.20      error ("Different versions of theory component " ^ quote (#2 id))
   12.21    else Inttab.update id ids;
   12.22  
   12.23 @@ -275,8 +275,7 @@
   12.24  
   12.25  val eq_thy = eq_id o pairself (#id o identity_of);
   12.26  
   12.27 -fun proper_subthy
   12.28 -    (Theory ({id = (i, _), ...}, _, _, _), Theory ({ids, iids, ...}, _, _, _)) =
   12.29 +fun proper_subthy (Theory ({id = (i, _), ...}, _, _, _), Theory ({ids, iids, ...}, _, _, _)) =
   12.30    Inttab.defined ids i orelse Inttab.defined iids i;
   12.31  
   12.32  fun subthy thys = eq_thy thys orelse proper_subthy thys;

    13.1 --- a/src/Tools/induct.ML	Fri Sep 26 17:24:15 2008 +0200
    13.2 +++ b/src/Tools/induct.ML	Fri Sep 26 19:07:56 2008 +0200
    13.3 @@ -478,7 +478,7 @@
    13.4            let
    13.5              val xs = rename_params (Logic.strip_params A);
    13.6              val xs' =
    13.7 -              (case List.filter (equal x) xs of
    13.8 +              (case filter (fn x' => x' = x) xs of
    13.9                  [] => xs | [_] => xs | _ => index 1 xs);
   13.10            in Logic.list_rename_params (xs', A) end;
   13.11          fun rename_prop p =