avoid polymorphic equality;
authorwenzelm
Tue Mar 21 12:18:15 2006 +0100 (2006-03-21)
changeset 193055c16895d548b
parent 19304 15f001295a7b
child 19306 73137c0b26f5
avoid polymorphic equality;
src/Pure/General/name_space.ML
src/Pure/General/path.ML
src/Pure/General/symbol.ML
src/Pure/General/url.ML
src/Pure/Isar/antiquote.ML
src/Pure/Isar/element.ML
src/Pure/Isar/outer_lex.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Proof/reconstruct.ML
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/type_ext.ML
src/Pure/Thy/html.ML
src/Pure/Thy/present.ML
src/Pure/Thy/thy_info.ML
src/Pure/pure_thy.ML
src/Pure/thm.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/General/name_space.ML	Tue Mar 21 12:18:13 2006 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Tue Mar 21 12:18:15 2006 +0100
     1.3 @@ -68,7 +68,7 @@
     1.4  val is_hidden = String.isPrefix "??."
     1.5  
     1.6  val separator = ".";
     1.7 -val is_qualified = exists_string (equal separator);
     1.8 +val is_qualified = exists_string (fn s => s = separator);
     1.9  
    1.10  val pack = space_implode separator;
    1.11  val unpack = space_explode separator;
    1.12 @@ -229,7 +229,7 @@
    1.13      error ("Attempt to declare hidden name " ^ quote name)
    1.14    else
    1.15      let val names = unpack name in
    1.16 -      conditional (null names orelse exists (equal "") names) (fn () =>
    1.17 +      conditional (null names orelse exists (fn s => s = "") names) (fn () =>
    1.18          error ("Bad name declaration " ^ quote name));
    1.19        fold (add_name name) (map pack (accs names)) space
    1.20      end;
     2.1 --- a/src/Pure/General/path.ML	Tue Mar 21 12:18:13 2006 +0100
     2.2 +++ b/src/Pure/General/path.ML	Tue Mar 21 12:18:15 2006 +0100
     2.3 @@ -118,7 +118,7 @@
     2.4          "$" :: cs => variable_elem cs
     2.5        | cs => basic_elem cs);
     2.6  
     2.7 -val unpack_elems = map unpack_elem o filter_out (equal "" orf equal ".");
     2.8 +val unpack_elems = map unpack_elem o filter_out (fn c => c = "" orelse c = ".");
     2.9  
    2.10  fun unpack str = Path (norm
    2.11    (case space_explode "/" str of
    2.12 @@ -140,7 +140,7 @@
    2.13    | ext e path = split_path (fn (prfx, s) => append (Path prfx) (basic (s ^ "." ^ e))) path;
    2.14  
    2.15  val split_ext = split_path (fn (prfx, s) => apfst (append (Path prfx))
    2.16 -  (case take_suffix (not_equal ".") (explode s) of
    2.17 +  (case take_suffix (fn c => c <> ".") (explode s) of
    2.18      ([], _) => (Path [Basic s], "")
    2.19    | (cs, e) => (Path [Basic (implode (Library.take (length cs - 1, cs)))], implode e)));
    2.20  
     3.1 --- a/src/Pure/General/symbol.ML	Tue Mar 21 12:18:13 2006 +0100
     3.2 +++ b/src/Pure/General/symbol.ML	Tue Mar 21 12:18:15 2006 +0100
     3.3 @@ -414,7 +414,7 @@
     3.4  (* source *)
     3.5  
     3.6  val recover =
     3.7 -  Scan.any ((not o is_blank) andf not_equal "\"" andf not_eof) >> K [malformed];
     3.8 +  Scan.any (fn s => not (is_blank s) andalso s <> "\"" andalso not_eof s) >> K [malformed];
     3.9  
    3.10  fun source do_recover src =
    3.11    Source.source stopper (Scan.bulk scan) (if do_recover then SOME recover else NONE) src;
    3.12 @@ -433,7 +433,7 @@
    3.13      else the (Scan.read stopper (Scan.repeat scan) chs)
    3.14    end;
    3.15  
    3.16 -val chars_only = not o exists_string (equal "\\");
    3.17 +val chars_only = not o exists_string (fn s => s = "\\");
    3.18  
    3.19  
    3.20  (* escape *)
     4.1 --- a/src/Pure/General/url.ML	Tue Mar 21 12:18:13 2006 +0100
     4.2 +++ b/src/Pure/General/url.ML	Tue Mar 21 12:18:15 2006 +0100
     4.3 @@ -53,7 +53,7 @@
     4.4  local
     4.5  
     4.6  val scan_host =
     4.7 -  (Scan.any1 (not_equal "/" andf Symbol.not_eof) >> implode) --|
     4.8 +  (Scan.any1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
     4.9    Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
    4.10  
    4.11  val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
     5.1 --- a/src/Pure/Isar/antiquote.ML	Tue Mar 21 12:18:13 2006 +0100
     5.2 +++ b/src/Pure/Isar/antiquote.ML	Tue Mar 21 12:18:15 2006 +0100
     5.3 @@ -36,8 +36,8 @@
     5.4  
     5.5  val scan_txt =
     5.6    T.scan_blank ||
     5.7 -  T.keep_line ($$ "@" --| Scan.ahead (Scan.one (not_equal "{"))) ||
     5.8 -  T.keep_line (Scan.one (not_equal "@" andf Symbol.not_sync andf Symbol.not_eof));
     5.9 +  T.keep_line ($$ "@" --| Scan.ahead (~$$ "{")) ||
    5.10 +  T.keep_line (Scan.one (fn s => s <> "@" andalso Symbol.not_sync s andalso Symbol.not_eof s));
    5.11  
    5.12  fun escape "\\" = "\\\\"
    5.13    | escape "\"" = "\\\""
    5.14 @@ -48,7 +48,7 @@
    5.15  val scan_ant =
    5.16    T.scan_blank ||
    5.17    T.scan_string >> quote_escape ||
    5.18 -  T.keep_line (Scan.one (not_equal "}" andf Symbol.not_sync andf Symbol.not_eof));
    5.19 +  T.keep_line (Scan.one (fn s => s <> "}" andalso Symbol.not_sync s andalso Symbol.not_eof s));
    5.20  
    5.21  val scan_antiq =
    5.22    T.keep_line ($$ "@" -- $$ "{") |--
     6.1 --- a/src/Pure/Isar/element.ML	Tue Mar 21 12:18:13 2006 +0100
     6.2 +++ b/src/Pure/Isar/element.ML	Tue Mar 21 12:18:15 2006 +0100
     6.3 @@ -342,7 +342,7 @@
     6.4  
     6.5      val vars = Term.add_vars raw_prop [];
     6.6      val frees = ProofContext.rename_frees ctxt [raw_prop] (map (apfst fst) vars);
     6.7 -    val fixes = rev (filter_out (equal AutoBind.thesisN o #1) frees);
     6.8 +    val fixes = rev (filter_out (fn (x, _) => x = AutoBind.thesisN) frees);
     6.9  
    6.10      val prop = Term.instantiate ([], vars ~~ map Free frees) raw_prop;
    6.11      val (prems, concl) = Logic.strip_horn prop;
     7.1 --- a/src/Pure/Isar/outer_lex.ML	Tue Mar 21 12:18:13 2006 +0100
     7.2 +++ b/src/Pure/Isar/outer_lex.ML	Tue Mar 21 12:18:15 2006 +0100
     7.3 @@ -214,8 +214,8 @@
     7.4    scan_blank ||
     7.5    keep_line ($$ "\\") |-- !!! "bad escape character in string"
     7.6        (scan_blank || keep_line ($$ q || $$ "\\")) ||
     7.7 -  keep_line (Scan.one (not_equal q andf not_equal "\\" andf
     7.8 -    Symbol.not_sync andf Symbol.not_eof));
     7.9 +  keep_line (Scan.one (fn s => s <> q andalso s <> "\\" andalso
    7.10 +    Symbol.not_sync s andalso Symbol.not_eof s));
    7.11  
    7.12  fun scan_strs q =
    7.13    keep_line ($$ q) |--
    7.14 @@ -234,8 +234,8 @@
    7.15  
    7.16  val scan_verb =
    7.17    scan_blank ||
    7.18 -  keep_line ($$ "*" --| Scan.ahead (Scan.one (not_equal "}"))) ||
    7.19 -  keep_line (Scan.one (not_equal "*" andf Symbol.not_sync andf Symbol.not_eof));
    7.20 +  keep_line ($$ "*" --| Scan.ahead (~$$ "}")) ||
    7.21 +  keep_line (Scan.one (fn s => s <> "*" andalso Symbol.not_sync s andalso Symbol.not_eof s));
    7.22  
    7.23  val scan_verbatim =
    7.24    keep_line ($$ "{" -- $$ "*") |--
    7.25 @@ -245,7 +245,7 @@
    7.26  
    7.27  (* scan space *)
    7.28  
    7.29 -val is_space = Symbol.is_blank andf not_equal "\n";
    7.30 +fun is_space s = Symbol.is_blank s andalso s <> "\n";
    7.31  
    7.32  val scan_space =
    7.33    (keep_line (Scan.any1 is_space) -- Scan.optional (incr_line ($$ "\n")) "" ||
    7.34 @@ -258,8 +258,9 @@
    7.35    Scan.lift scan_blank ||
    7.36    Scan.depend (fn d => keep_line ($$ "(" ^^ $$ "*") >> pair (d + 1)) ||
    7.37    Scan.depend (fn 0 => Scan.fail | d => keep_line ($$ "*" ^^ $$ ")") >> pair (d - 1)) ||
    7.38 -  Scan.lift (keep_line ($$ "*" --| Scan.ahead (Scan.one (not_equal ")")))) ||
    7.39 -  Scan.lift (keep_line (Scan.one (not_equal "*" andf Symbol.not_sync andf Symbol.not_eof)));
    7.40 +  Scan.lift (keep_line ($$ "*" --| Scan.ahead (~$$ ")"))) ||
    7.41 +  Scan.lift (keep_line (Scan.one (fn s =>
    7.42 +    s <> "*" andalso Symbol.not_sync s andalso Symbol.not_eof s)));
    7.43  
    7.44  val scan_comment =
    7.45    keep_line ($$ "(" -- $$ "*") |--
     8.1 --- a/src/Pure/Proof/extraction.ML	Tue Mar 21 12:18:13 2006 +0100
     8.2 +++ b/src/Pure/Proof/extraction.ML	Tue Mar 21 12:18:15 2006 +0100
     8.3 @@ -84,7 +84,7 @@
     8.4  
     8.5  fun merge_rules
     8.6    ({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) =
     8.7 -  foldr add_rule {next = next, rs = rs1, net = net} (rs2 \\ rs1);
     8.8 +  foldr add_rule {next = next, rs = rs1, net = net} (subtract (op =) rs1 rs2);
     8.9  
    8.10  fun condrew thy rules procs =
    8.11    let
    8.12 @@ -205,7 +205,7 @@
    8.13      {realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
    8.14       typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
    8.15       types = merge_alists types1 types2,
    8.16 -     realizers = Symtab.merge_list (eq_set o pairself #1) (realizers1, realizers2),
    8.17 +     realizers = Symtab.merge_list (gen_eq_set (op =) o pairself #1) (realizers1, realizers2),
    8.18       defs = gen_merge_lists eq_thm defs1 defs2,
    8.19       expand = merge_lists expand1 expand2,
    8.20       prep = (case prep1 of NONE => prep2 | _ => prep1)};
    8.21 @@ -483,7 +483,7 @@
    8.22  
    8.23        in foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
    8.24  
    8.25 -    fun find vs = Option.map snd o find_first (curry eq_set vs o fst);
    8.26 +    fun find vs = Option.map snd o find_first (curry (gen_eq_set (op =)) vs o fst);
    8.27      fun find' s = map snd o List.filter (equal s o fst)
    8.28  
    8.29      fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw
     9.1 --- a/src/Pure/Proof/proof_syntax.ML	Tue Mar 21 12:18:13 2006 +0100
     9.2 +++ b/src/Pure/Proof/proof_syntax.ML	Tue Mar 21 12:18:15 2006 +0100
     9.3 @@ -111,7 +111,7 @@
     9.4        | rename (prf' as PThm ((s, tags), prf, prop, Ts)) =
     9.5            let
     9.6              val prop' = if_none (AList.lookup (op =) thms' s) (Bound 0);
     9.7 -            val ps = map fst (the (Symtab.lookup thms s)) \ prop'
     9.8 +            val ps = remove (op =) prop' (map fst (the (Symtab.lookup thms s)))
     9.9            in if prop = prop' then prf' else
    9.10              PThm ((s ^ "_" ^ string_of_int (length ps - find_index_eq prop ps), tags),
    9.11                prf, prop, Ts)
    9.12 @@ -248,7 +248,8 @@
    9.13  
    9.14  fun proof_syntax prf =
    9.15    let
    9.16 -    val thm_names = map fst (Symtab.dest (thms_of_proof prf Symtab.empty)) \ "";
    9.17 +    val thm_names = filter_out (equal "")
    9.18 +      (map fst (Symtab.dest (thms_of_proof prf Symtab.empty)));
    9.19      val axm_names = map fst (Symtab.dest (axms_of_proof prf Symtab.empty));
    9.20    in
    9.21      add_proof_syntax #>
    10.1 --- a/src/Pure/Proof/reconstruct.ML	Tue Mar 21 12:18:13 2006 +0100
    10.2 +++ b/src/Pure/Proof/reconstruct.ML	Tue Mar 21 12:18:15 2006 +0100
    10.3 @@ -246,7 +246,7 @@
    10.4        (Vartab.foldl (add_term_ixns o apsnd (snd o snd)) ([], asol), iTs);
    10.5      fun check_cs [] = []
    10.6        | check_cs ((u, p, vs)::ps) =
    10.7 -          let val vs' = vs \\ dom;
    10.8 +          let val vs' = subtract (op =) dom vs;
    10.9            in if vs = vs' then (u, p, vs)::check_cs ps
   10.10               else (true, p, vs' union vran)::check_cs ps
   10.11            end
    11.1 --- a/src/Pure/Syntax/lexicon.ML	Tue Mar 21 12:18:13 2006 +0100
    11.2 +++ b/src/Pure/Syntax/lexicon.ML	Tue Mar 21 12:18:15 2006 +0100
    11.3 @@ -222,8 +222,8 @@
    11.4  
    11.5  val scan_chr =
    11.6    $$ "\\" |-- Scan.one Symbol.not_eof ||
    11.7 -  Scan.one (not_equal "'" andf Symbol.not_eof) ||
    11.8 -  $$ "'" --| Scan.ahead (Scan.one (not_equal "'"));
    11.9 +  Scan.one (fn s => s <> "'" andalso Symbol.not_eof s) ||
   11.10 +  $$ "'" --| Scan.ahead (~$$ "'");
   11.11  
   11.12  val scan_str =
   11.13    $$ "'" |-- $$ "'" |-- !! (lex_err "missing end of string" "''")
   11.14 @@ -243,8 +243,8 @@
   11.15  val scan_cmt =
   11.16    Scan.depend (fn d => $$ "(" ^^ $$ "*" >> pair (d + 1)) ||
   11.17    Scan.depend (fn 0 => Scan.fail | d => $$ "*" ^^ $$ ")" >> pair (d - 1)) ||
   11.18 -  Scan.lift ($$ "*" --| Scan.ahead (Scan.one (not_equal ")"))) ||
   11.19 -  Scan.lift (Scan.one (not_equal "*" andf Symbol.not_eof));
   11.20 +  Scan.lift ($$ "*" --| Scan.ahead (~$$ ")")) ||
   11.21 +  Scan.lift (Scan.one (fn s => s <> "*" andalso Symbol.not_eof s));
   11.22  
   11.23  val scan_comment =
   11.24    $$ "(" -- $$ "*" -- !! (lex_err "missing end of comment" "(*")
    12.1 --- a/src/Pure/Syntax/parser.ML	Tue Mar 21 12:18:13 2006 +0100
    12.2 +++ b/src/Pure/Syntax/parser.ML	Tue Mar 21 12:18:15 2006 +0100
    12.3 @@ -60,7 +60,7 @@
    12.4     (used for expanding chain list)*)
    12.5  fun connected_with _ [] relatives = relatives
    12.6    | connected_with chains (root :: roots) relatives =
    12.7 -    let val branches = these (AList.lookup (op =) chains root) \\ relatives;
    12.8 +    let val branches = subtract (op =) relatives (these (AList.lookup (op =) chains root));
    12.9      in connected_with chains (branches @ roots) (branches @ relatives) end;
   12.10  
   12.11  (* convert productions to grammar;
   12.12 @@ -93,7 +93,7 @@
   12.13                  let
   12.14                    val ((to_nts, to_tks), ps) = Array.sub (prods, to);
   12.15  
   12.16 -                  val new_tks = from_tks \\ to_tks;  (*added lookahead tokens*)
   12.17 +                  val new_tks = subtract (op =) to_tks from_tks;  (*added lookahead tokens*)
   12.18                  in Array.update (prods, to, ((to_nts, to_tks @ new_tks), ps));
   12.19                     copy_lookahead tos (if null new_tks then added
   12.20                                         else (to, new_tks) :: added)
   12.21 @@ -149,9 +149,9 @@
   12.22                        let
   12.23                          val new_lambda = is_none tk andalso nts subset lambdas;
   12.24  
   12.25 -                        val new_tks = (if is_some tk then [the tk] else []) @
   12.26 -                          Library.foldl token_union ([], map starts_for_nt nts) \\
   12.27 -                          l_starts;
   12.28 +                        val new_tks = subtract (op =) l_starts
   12.29 +                          ((if is_some tk then [the tk] else []) @
   12.30 +                            Library.foldl token_union ([], map starts_for_nt nts));
   12.31  
   12.32                          val added_tks' = token_union (new_tks, added_tks);
   12.33  
   12.34 @@ -199,7 +199,7 @@
   12.35                        val (add_lambda, nt_dependencies, added_tks, nt_prods') =
   12.36                          examine_prods tk_prods false [] [] nt_prods;
   12.37  
   12.38 -                      val added_nts = nt_dependencies \\ old_nts;
   12.39 +                      val added_nts = subtract (op =) old_nts nt_dependencies;
   12.40  
   12.41                        val added_lambdas' =
   12.42                          if add_lambda then nt :: added_lambdas
   12.43 @@ -222,11 +222,11 @@
   12.44                  val (added_lambdas, added_starts') =
   12.45                    process_nts dependent [] added_starts;
   12.46  
   12.47 -                val added_lambdas' = added_lambdas \\ lambdas;
   12.48 +                val added_lambdas' = subtract (op =) lambdas added_lambdas;
   12.49                in propagate_lambda (ls @ added_lambdas') added_starts'
   12.50                                    (added_lambdas' @ lambdas)
   12.51                end;
   12.52 -        in propagate_lambda (lambdas' \\ lambdas) added_starts lambdas' end;
   12.53 +        in propagate_lambda (subtract (op =) lambdas lambdas') added_starts lambdas' end;
   12.54  
   12.55        (*insert production into grammar*)
   12.56        val (added_starts', prod_count') =
   12.57 @@ -748,8 +748,7 @@
   12.58              val dummy =
   12.59                if not (!warned) andalso
   12.60                   length (new_states @ States) > (!branching_level) then
   12.61 -                (warning "Currently parsed expression could be \
   12.62 -                         \extremely ambiguous.";
   12.63 +                (warning "Currently parsed expression could be extremely ambiguous.";
   12.64                   warned := true)
   12.65                else ();
   12.66            in
    13.1 --- a/src/Pure/Syntax/syn_ext.ML	Tue Mar 21 12:18:13 2006 +0100
    13.2 +++ b/src/Pure/Syntax/syn_ext.ML	Tue Mar 21 12:18:15 2006 +0100
    13.3 @@ -217,7 +217,7 @@
    13.4    scan_sym >> SOME ||
    13.5    $$ "'" -- Scan.one Symbol.is_blank >> K NONE;
    13.6  
    13.7 -val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (Scan.one (not_equal "'"));
    13.8 +val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'");
    13.9  val read_symbs = List.mapPartial I o the o Scan.read Symbol.stopper scan_symbs;
   13.10  
   13.11  fun unique_index xsymbs =
    14.1 --- a/src/Pure/Syntax/type_ext.ML	Tue Mar 21 12:18:13 2006 +0100
    14.2 +++ b/src/Pure/Syntax/type_ext.ML	Tue Mar 21 12:18:15 2006 +0100
    14.3 @@ -140,14 +140,14 @@
    14.4  val no_bracketsN = "no_brackets";
    14.5  
    14.6  fun no_brackets () =
    14.7 -  find_first (equal bracketsN orf equal no_bracketsN) (! print_mode)
    14.8 +  find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN) (! print_mode)
    14.9      = SOME no_bracketsN;
   14.10  
   14.11  val type_bracketsN = "type_brackets";
   14.12  val no_type_bracketsN = "no_type_brackets";
   14.13  
   14.14  fun no_type_brackets () =
   14.15 -  Library.find_first (equal type_bracketsN orf equal no_type_bracketsN) (! print_mode)
   14.16 +  find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN) (! print_mode)
   14.17      <> SOME type_bracketsN;
   14.18  
   14.19  
    15.1 --- a/src/Pure/Thy/html.ML	Tue Mar 21 12:18:13 2006 +0100
    15.2 +++ b/src/Pure/Thy/html.ML	Tue Mar 21 12:18:15 2006 +0100
    15.3 @@ -223,7 +223,7 @@
    15.4  in
    15.5  
    15.6  fun output_width str =
    15.7 -  if not (exists_string (equal "\\" orf equal "<" orf equal ">" orf equal "&") str)
    15.8 +  if not (exists_string (fn s => s = "\\" orelse s = "<" orelse s = ">" orelse s = "&") str)
    15.9    then Symbol.default_output str
   15.10    else
   15.11      let val (syms, width) = fold_map (fn (w, s) => fn width => (s, w + width))
    16.1 --- a/src/Pure/Thy/present.ML	Tue Mar 21 12:18:13 2006 +0100
    16.2 +++ b/src/Pure/Thy/present.ML	Tue Mar 21 12:18:15 2006 +0100
    16.3 @@ -261,7 +261,7 @@
    16.4  fun update_index dir name =
    16.5    (case try get_entries dir of
    16.6      NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.pack dir))
    16.7 -  | SOME es => (put_entries ((es \ name) @ [name]) dir; create_index dir));
    16.8 +  | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir));
    16.9  
   16.10  
   16.11  (* document versions *)
    17.1 --- a/src/Pure/Thy/thy_info.ML	Tue Mar 21 12:18:13 2006 +0100
    17.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Mar 21 12:18:15 2006 +0100
    17.3 @@ -171,8 +171,8 @@
    17.4  fun relevant_names names =
    17.5    let
    17.6      val (finished, unfinished) =
    17.7 -      List.filter (equal Context.draftN orf known_thy) names
    17.8 -      |> List.partition (not_equal Context.draftN andf is_finished);
    17.9 +      List.filter (fn name => name = Context.draftN orelse known_thy name) names
   17.10 +      |> List.partition (fn name => name <> Context.draftN andalso is_finished name);
   17.11    in (if not (null finished) then [List.last finished] else []) @ unfinished end;
   17.12  
   17.13  in
    18.1 --- a/src/Pure/pure_thy.ML	Tue Mar 21 12:18:13 2006 +0100
    18.2 +++ b/src/Pure/pure_thy.ML	Tue Mar 21 12:18:15 2006 +0100
    18.3 @@ -107,7 +107,7 @@
    18.4    Thm.put_name_tags (Thm.name_of_thm thm, f (#2 (Thm.get_name_tags thm))) thm;
    18.5  
    18.6  fun tag_rule tg = map_tags (fn tgs => if tg mem tgs then tgs else tgs @ [tg]);
    18.7 -fun untag_rule s = map_tags (filter_out (equal s o #1));
    18.8 +fun untag_rule s = map_tags (filter_out (fn (s', _) => s = s'));
    18.9  
   18.10  fun tag tg x = Thm.rule_attribute (K (tag_rule tg)) x;
   18.11  fun untag s x = Thm.rule_attribute (K (untag_rule s)) x;
    19.1 --- a/src/Pure/thm.ML	Tue Mar 21 12:18:13 2006 +0100
    19.2 +++ b/src/Pure/thm.ML	Tue Mar 21 12:18:15 2006 +0100
    19.3 @@ -450,7 +450,7 @@
    19.4  val concl_of = Logic.strip_imp_concl o prop_of;
    19.5  val prems_of = Logic.strip_imp_prems o prop_of;
    19.6  fun nprems_of th = Logic.count_prems (prop_of th, 0);
    19.7 -val no_prems = equal 0 o nprems_of;
    19.8 +fun no_prems th = nprems_of th = 0;
    19.9  
   19.10  fun major_prem_of th =
   19.11    (case prems_of th of
    20.1 --- a/src/Pure/type.ML	Tue Mar 21 12:18:13 2006 +0100
    20.2 +++ b/src/Pure/type.ML	Tue Mar 21 12:18:15 2006 +0100
    20.3 @@ -220,7 +220,8 @@
    20.4  
    20.5  fun varify (t, fixed) =
    20.6    let
    20.7 -    val fs = add_term_tfrees (t, []) \\ fixed;
    20.8 +    val fs = Term.fold_types (Term.fold_atyps
    20.9 +      (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
   20.10      val ixns = add_term_tvar_ixns (t, []);
   20.11      val fmap = fs ~~ map (rpair 0) (variantlist (map fst fs, map #1 ixns))
   20.12      fun thaw (f as (a, S)) =