slight adaptions to library changes
authorhaftmann
Tue Sep 20 08:21:49 2005 +0200 (2005-09-20)
changeset 1749626535df536ae
parent 17495 ddb14cbec6a2
child 17497 539319bd6162
slight adaptions to library changes
src/CTT/CTT.ML
src/CTT/rew.ML
src/FOL/intprover.ML
src/FOLP/classical.ML
src/FOLP/intprover.ML
src/HOL/Tools/recdef_package.ML
src/Provers/Arith/fast_lin_arith.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/term_style.ML
src/Pure/Syntax/syntax.ML
src/Pure/Thy/present.ML
src/Pure/Thy/thy_parse.ML
src/Pure/axclass.ML
src/Pure/meta_simplifier.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
src/Pure/tactic.ML
src/Pure/theory.ML
src/Pure/type.ML
src/Pure/type_infer.ML
     1.1 --- a/src/CTT/CTT.ML	Tue Sep 20 08:20:22 2005 +0200
     1.2 +++ b/src/CTT/CTT.ML	Tue Sep 20 08:21:49 2005 +0200
     1.3 @@ -157,7 +157,7 @@
     1.4  
     1.5  (*0 subgoals vs 1 or more*)
     1.6  val (safe0_brls, safep_brls) =
     1.7 -    List.partition (apl(0,op=) o subgoals_of_brl) safe_brls;
     1.8 +    List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
     1.9  
    1.10  fun safestep_tac thms i =
    1.11      form_tac  ORELSE
     2.1 --- a/src/CTT/rew.ML	Tue Sep 20 08:20:22 2005 +0200
     2.2 +++ b/src/CTT/rew.ML	Tue Sep 20 08:21:49 2005 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  (*Make list of ProdE RS ProdE ... RS ProdE RS EqE
     2.5    for using assumptions as rewrite rules*)
     2.6  fun peEs 0 = []
     2.7 -  | peEs n = EqE :: map (apl(ProdE, op RS)) (peEs (n-1));
     2.8 +  | peEs n = EqE :: map (curry (op RS) ProdE) (peEs (n-1));
     2.9  
    2.10  (*Tactic used for proving conditions for the cond_rls*)
    2.11  val prove_cond_tac = eresolve_tac (peEs 5);
     3.1 --- a/src/FOL/intprover.ML	Tue Sep 20 08:20:22 2005 +0200
     3.2 +++ b/src/FOL/intprover.ML	Tue Sep 20 08:21:49 2005 +0200
     3.3 @@ -60,7 +60,7 @@
     3.4  
     3.5  (*0 subgoals vs 1 or more: the p in safep is for positive*)
     3.6  val (safe0_brls, safep_brls) =
     3.7 -    List.partition (apl(0,op=) o subgoals_of_brl) safe_brls;
     3.8 +    List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
     3.9  
    3.10  (*Attack subgoals using safe inferences -- matching, not resolution*)
    3.11  val safe_step_tac = FIRST' [eq_assume_tac,
     4.1 --- a/src/FOLP/classical.ML	Tue Sep 20 08:20:22 2005 +0200
     4.2 +++ b/src/FOLP/classical.ML	Tue Sep 20 08:21:49 2005 +0200
     4.3 @@ -112,7 +112,7 @@
     4.4  (*Note that allE precedes exI in haz_brls*)
     4.5  fun make_cs {safeIs,safeEs,hazIs,hazEs} =
     4.6    let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*)
     4.7 -          List.partition (apl(0,op=) o subgoals_of_brl) 
     4.8 +          List.partition (curry (op =) 0 o subgoals_of_brl) 
     4.9               (sort (make_ord lessb) (joinrules(safeIs, safeEs)))
    4.10    in CS{safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs,
    4.11          safe0_brls=safe0_brls, safep_brls=safep_brls,
     5.1 --- a/src/FOLP/intprover.ML	Tue Sep 20 08:20:22 2005 +0200
     5.2 +++ b/src/FOLP/intprover.ML	Tue Sep 20 08:21:49 2005 +0200
     5.3 @@ -50,7 +50,7 @@
     5.4  
     5.5  (*0 subgoals vs 1 or more: the p in safep is for positive*)
     5.6  val (safe0_brls, safep_brls) =
     5.7 -    List.partition (apl(0,op=) o subgoals_of_brl) safe_brls;
     5.8 +    List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
     5.9  
    5.10  (*Attack subgoals using safe inferences*)
    5.11  val safe_step_tac = FIRST' [uniq_assume_tac,
     6.1 --- a/src/HOL/Tools/recdef_package.ML	Tue Sep 20 08:20:22 2005 +0200
     6.2 +++ b/src/HOL/Tools/recdef_package.ML	Tue Sep 20 08:21:49 2005 +0200
     6.3 @@ -245,7 +245,7 @@
     6.4      val (thy, {rules = rules_idx, induct, tcs}) =
     6.5          tfl_fn strict thy cs (ss delcongs [imp_cong])
     6.6                 congs wfs name R eqs;
     6.7 -    val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx);
     6.8 +    val rules = map (map #1) (Library.partition_eq (Library.eq_snd (op =)) rules_idx);
     6.9      val simp_att = if null tcs then
    6.10        [Simplifier.simp_add_global, RecfunCodegen.add NONE] else [];
    6.11  
     7.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Tue Sep 20 08:20:22 2005 +0200
     7.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Sep 20 08:21:49 2005 +0200
     7.3 @@ -278,7 +278,7 @@
     7.4    if n = 1 then i
     7.5    else if n = 0 andalso ty = Lt then sys_error "multiply_ineq"
     7.6    else if n < 0 andalso (ty=Le orelse ty=Lt) then sys_error "multiply_ineq"
     7.7 -  else Lineq(n * k,ty,map (apl(n,op * )) l,Multiplied(n,just));
     7.8 +  else Lineq (n * k, ty, map (curry (op *) n) l, Multiplied (n, just));
     7.9  
    7.10  (* ------------------------------------------------------------------------- *)
    7.11  (* Add together (in)equations.                                               *)
    7.12 @@ -317,7 +317,7 @@
    7.13    case ty  of Eq => k <> 0 | Le => k > 0 | Lt => k >= 0;
    7.14  
    7.15  fun calc_blowup (l:IntInf.int list) =
    7.16 -  let val (p,n) = List.partition (apl(0,op<)) (List.filter (apl(0,op<>)) l)
    7.17 +  let val (p,n) = List.partition (curry (op <) 0) (List.filter (curry (op <>) 0) l)
    7.18    in (length p) * (length n) end;
    7.19  
    7.20  (* ------------------------------------------------------------------------- *)
    7.21 @@ -538,11 +538,11 @@
    7.22    in a ^ " = " ^ s end;
    7.23  
    7.24  fun print_ex sds =
    7.25 -  tracing o
    7.26 -  apl("Counter example:\n",op ^) o
    7.27 -  commas o
    7.28 -  map print_atom o
    7.29 -  apl(sds, op ~~);
    7.30 +  curry (op ~~) sds
    7.31 +  #> map print_atom
    7.32 +  #> commas
    7.33 +  #> curry (op ^) "Counter example:\n"
    7.34 +  #> tracing;
    7.35  
    7.36  fun trace_ex(sg,params,atoms,discr,n,hist:history) =
    7.37    if null hist then ()
     8.1 --- a/src/Pure/Isar/attrib.ML	Tue Sep 20 08:20:22 2005 +0200
     8.2 +++ b/src/Pure/Isar/attrib.ML	Tue Sep 20 08:21:49 2005 +0200
     8.3 @@ -72,7 +72,7 @@
     8.4    val copy = I;
     8.5    val extend = I;
     8.6  
     8.7 -  fun merge _ tables = NameSpace.merge_tables eq_snd tables handle Symtab.DUPS dups =>
     8.8 +  fun merge _ tables = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
     8.9      error ("Attempt to merge different versions of attribute(s) " ^ commas_quote dups);
    8.10  
    8.11    fun print _ attribs =
     9.1 --- a/src/Pure/Isar/context_rules.ML	Tue Sep 20 08:20:22 2005 +0200
     9.2 +++ b/src/Pure/Isar/context_rules.ML	Tue Sep 20 08:21:49 2005 +0200
     9.3 @@ -131,7 +131,7 @@
     9.4    fun merge _ (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
     9.5        Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
     9.6      let
     9.7 -      val wrappers = (gen_merge_lists' eq_snd ws1 ws2, gen_merge_lists' eq_snd ws1' ws2');
     9.8 +      val wrappers = (gen_merge_lists' (eq_snd (op =)) ws1 ws2, gen_merge_lists' (eq_snd (op =)) ws1' ws2');
     9.9        val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) =>
    9.10            k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) rules1 rules2;
    9.11        val next = ~ (length rules);
    10.1 --- a/src/Pure/Isar/locale.ML	Tue Sep 20 08:20:22 2005 +0200
    10.2 +++ b/src/Pure/Isar/locale.ML	Tue Sep 20 08:21:49 2005 +0200
    10.3 @@ -372,7 +372,7 @@
    10.4    fun join_locs _ ({predicate, import, elems, params, regs}: locale,
    10.5        {elems = elems', regs = regs', ...}: locale) =
    10.6      SOME {predicate = predicate, import = import,
    10.7 -      elems = gen_merge_lists eq_snd elems elems',
    10.8 +      elems = gen_merge_lists (eq_snd (op =)) elems elems',
    10.9        params = params,
   10.10        regs = merge_alists regs regs'};
   10.11    fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
   10.12 @@ -770,10 +770,10 @@
   10.13      val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (List.mapPartial I Vs));
   10.14    in map (Option.map (Envir.norm_type unifier')) Vs end;
   10.15  
   10.16 -fun params_of elemss = gen_distinct eq_fst (List.concat (map (snd o fst) elemss));
   10.17 -fun params_of' elemss = gen_distinct eq_fst (List.concat (map (snd o fst o fst) elemss));
   10.18 +fun params_of elemss = gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss));
   10.19 +fun params_of' elemss = gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst o fst) elemss));
   10.20  fun params_syn_of syn elemss =
   10.21 -  gen_distinct eq_fst (List.concat (map (snd o fst) elemss)) |>
   10.22 +  gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss)) |>
   10.23      map (apfst (fn x => (x, valOf (Symtab.lookup syn x))));
   10.24  
   10.25  
   10.26 @@ -843,7 +843,7 @@
   10.27      val (unifier, _) = Library.foldl unify_list
   10.28        ((Vartab.empty, maxidx), map #2 (Symtab.dest (Symtab.make_multi parms)));
   10.29  
   10.30 -    val parms' = map (apsnd (Envir.norm_type unifier)) (gen_distinct eq_fst parms);
   10.31 +    val parms' = map (apsnd (Envir.norm_type unifier)) (gen_distinct (eq_fst (op =)) parms);
   10.32      val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
   10.33  
   10.34      fun inst_parms (i, ps) =
   10.35 @@ -939,7 +939,7 @@
   10.36              (* propagate parameter types, to keep them consistent *)
   10.37            val regs' = map (fn ((name, ps), ths) =>
   10.38                ((name, map (rename ren) ps), ths)) regs;
   10.39 -          val new_regs = gen_rems eq_fst (regs', ids);
   10.40 +          val new_regs = gen_rems (eq_fst (op =)) (regs', ids);
   10.41            val new_ids = map fst new_regs;
   10.42            val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) ps) p)))) new_ids;
   10.43  
   10.44 @@ -993,7 +993,7 @@
   10.45              val ren = renaming xs parms'
   10.46                handle ERROR_MESSAGE msg => err_in_locale' ctxt msg ids';
   10.47  
   10.48 -            val ids'' = gen_distinct eq_fst (map (rename_parms top ren) ids');
   10.49 +            val ids'' = gen_distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
   10.50              val parms'' = distinct (List.concat (map (#2 o #1) ids''));
   10.51              val syn'' = syn' |> Symtab.dest |> map (rename_var ren) |>
   10.52                    Symtab.make;
   10.53 @@ -1037,7 +1037,7 @@
   10.54  
   10.55      (* compute identifiers and syntax, merge with previous ones *)
   10.56      val (ids, _, syn) = identify true expr;
   10.57 -    val idents = gen_rems eq_fst (ids, prev_idents);
   10.58 +    val idents = gen_rems (eq_fst (op =)) (ids, prev_idents);
   10.59      val syntax = merge_syntax ctxt ids (syn, prev_syntax);
   10.60      (* add types to params, check for unique params and unify them *)
   10.61      val raw_elemss = unique_parms ctxt (map (eval syntax) idents);
    11.1 --- a/src/Pure/Isar/method.ML	Tue Sep 20 08:20:22 2005 +0200
    11.2 +++ b/src/Pure/Isar/method.ML	Tue Sep 20 08:21:49 2005 +0200
    11.3 @@ -541,7 +541,7 @@
    11.4    val empty = NameSpace.empty_table;
    11.5    val copy = I;
    11.6    val extend = I;
    11.7 -  fun merge _ tables = NameSpace.merge_tables eq_snd tables handle Symtab.DUPS dups =>
    11.8 +  fun merge _ tables = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
    11.9      error ("Attempt to merge different versions of method(s) " ^ commas_quote dups);
   11.10  
   11.11    fun print _ meths =
    12.1 --- a/src/Pure/Isar/proof_context.ML	Tue Sep 20 08:20:22 2005 +0200
    12.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Sep 20 08:21:49 2005 +0200
    12.3 @@ -958,7 +958,7 @@
    12.4  fun lthms_containing ctxt spec =
    12.5    FactIndex.find (fact_index_of ctxt) spec
    12.6    |> List.filter (valid_thms ctxt)
    12.7 -  |> gen_distinct eq_fst;
    12.8 +  |> gen_distinct (eq_fst (op =));
    12.9  
   12.10  
   12.11  (* name space operations *)
    13.1 --- a/src/Pure/Isar/term_style.ML	Tue Sep 20 08:20:22 2005 +0200
    13.2 +++ b/src/Pure/Isar/term_style.ML	Tue Sep 20 08:21:49 2005 +0200
    13.3 @@ -28,7 +28,7 @@
    13.4    val empty = Symtab.empty;
    13.5    val copy = I;
    13.6    val extend = I;
    13.7 -  fun merge _ tabs = Symtab.merge eq_snd tabs
    13.8 +  fun merge _ tabs = Symtab.merge (eq_snd (op =)) tabs
    13.9      handle Symtab.DUPS dups => err_dup_styles dups;
   13.10    fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab));
   13.11  end);
    14.1 --- a/src/Pure/Syntax/syntax.ML	Tue Sep 20 08:20:22 2005 +0200
    14.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Sep 20 08:21:49 2005 +0200
    14.3 @@ -108,7 +108,7 @@
    14.4  (** tables of token translation functions **)
    14.5  
    14.6  fun lookup_tokentr tabs modes =
    14.7 -  let val trs = gen_distinct eq_fst
    14.8 +  let val trs = gen_distinct (eq_fst (op =))
    14.9      (List.concat (map (these o AList.lookup (op =) tabs) (modes @ [""])))
   14.10    in fn c => Option.map fst (AList.lookup (op =) trs c) end;
   14.11  
   14.12 @@ -124,7 +124,7 @@
   14.13          val trs2 = these (AList.lookup (op =) tabs2 mode);
   14.14          val trs = gen_distinct eq_tr (trs1 @ trs2);
   14.15        in
   14.16 -        (case gen_duplicates eq_fst trs of
   14.17 +        (case gen_duplicates (eq_fst (op =)) trs of
   14.18            [] => (mode, trs)
   14.19          | dups => error ("More than one token translation function in mode " ^
   14.20              quote mode ^ " for " ^ commas_quote (map name dups)))
    15.1 --- a/src/Pure/Thy/present.ML	Tue Sep 20 08:20:22 2005 +0200
    15.2 +++ b/src/Pure/Thy/present.ML	Tue Sep 20 08:21:49 2005 +0200
    15.3 @@ -274,7 +274,7 @@
    15.4    | _ => error ("Malformed document version specification: " ^ quote str));
    15.5  
    15.6  fun read_versions strs =
    15.7 -  rev (gen_distinct eq_fst (rev ((documentN, "") :: map read_version strs)))
    15.8 +  rev (gen_distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_version strs)))
    15.9    |> filter_out (equal "-" o #2);
   15.10  
   15.11  
    16.1 --- a/src/Pure/Thy/thy_parse.ML	Tue Sep 20 08:20:22 2005 +0200
    16.2 +++ b/src/Pure/Thy/thy_parse.ML	Tue Sep 20 08:21:49 2005 +0200
    16.3 @@ -284,8 +284,8 @@
    16.4        [(parens (commas [t, mk_list xs, rhs, syn]), true)];
    16.5  
    16.6  fun mk_type_decls tys =
    16.7 -  "|> Theory.add_types\n" ^ mk_big_list (keyfilter tys false) ^ "\n\n\
    16.8 -  \|> Theory.add_tyabbrs\n" ^ mk_big_list (keyfilter tys true);
    16.9 +  "|> Theory.add_types\n" ^ mk_big_list (AList.find (op =) tys false) ^ "\n\n\
   16.10 +  \|> Theory.add_tyabbrs\n" ^ mk_big_list (AList.find (op =) tys true);
   16.11  
   16.12  
   16.13  val old_type_decl = names1 -- nat -- opt_infix >> mk_old_type_decl;
   16.14 @@ -390,8 +390,8 @@
   16.15  (* instance *)
   16.16  
   16.17  fun mk_witness (axths, opt_tac) =
   16.18 -  mk_list (keyfilter axths false) ^ "\n" ^
   16.19 -  mk_list (keyfilter axths true) ^ "\n" ^
   16.20 +  mk_list (AList.find (op =) axths false) ^ "\n" ^
   16.21 +  mk_list (AList.find (op =) axths true) ^ "\n" ^
   16.22    opt_tac;
   16.23  
   16.24  val axm_or_thm =
   16.25 @@ -441,7 +441,7 @@
   16.26  fun make_syntax keywords sects =
   16.27    let
   16.28      val dups = duplicates (map fst sects);
   16.29 -    val sects' = gen_distinct eq_fst sects;
   16.30 +    val sects' = gen_distinct (eq_fst (op =)) sects;
   16.31      val keys = map Symbol.explode (map fst sects' @ keywords);
   16.32    in
   16.33      if null dups then ()
    17.1 --- a/src/Pure/axclass.ML	Tue Sep 20 08:20:22 2005 +0200
    17.2 +++ b/src/Pure/axclass.ML	Tue Sep 20 08:21:49 2005 +0200
    17.3 @@ -103,7 +103,7 @@
    17.4          Type (t, tys) => (t, map dest_varT tys handle TYPE _ => err ())
    17.5        | _ => err ());
    17.6      val ss =
    17.7 -      if null (gen_duplicates eq_fst tvars)
    17.8 +      if null (gen_duplicates (eq_fst (op =)) tvars)
    17.9        then map snd tvars else err ();
   17.10    in (t, ss, c) end;
   17.11  
    18.1 --- a/src/Pure/meta_simplifier.ML	Tue Sep 20 08:20:22 2005 +0200
    18.2 +++ b/src/Pure/meta_simplifier.ML	Tue Sep 20 08:21:49 2005 +0200
    18.3 @@ -292,7 +292,7 @@
    18.4      val cngs = map (fn (name, {thm, ...}) => (name, thm)) (#1 congs);
    18.5      val prcs = Net.entries procs |>
    18.6        map (fn Proc {name, lhs, id, ...} => ((name, lhs), id))
    18.7 -      |> partition_eq eq_snd
    18.8 +      |> partition_eq (eq_snd (op =))
    18.9        |> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps))
   18.10        |> Library.sort_wrt #1;
   18.11    in
    19.1 --- a/src/Pure/pure_thy.ML	Tue Sep 20 08:20:22 2005 +0200
    19.2 +++ b/src/Pure/pure_thy.ML	Tue Sep 20 08:21:49 2005 +0200
    19.3 @@ -250,7 +250,7 @@
    19.4    |> map (fn thy =>
    19.5        FactIndex.find (fact_index_of thy) spec
    19.6        |> List.filter (fn (name, ths) => valid_thms theory (Name name, ths))
    19.7 -      |> gen_distinct eq_fst)
    19.8 +      |> gen_distinct (eq_fst (op =)))
    19.9    |> List.concat;
   19.10  
   19.11  fun thms_containing_consts thy consts =
    20.1 --- a/src/Pure/sign.ML	Tue Sep 20 08:20:22 2005 +0200
    20.2 +++ b/src/Pure/sign.ML	Tue Sep 20 08:21:49 2005 +0200
    20.3 @@ -227,7 +227,7 @@
    20.4        val naming = NameSpace.default_naming;
    20.5        val syn = Syntax.merge_syntaxes syn1 syn2;
    20.6        val tsig = Type.merge_tsigs pp (tsig1, tsig2);
    20.7 -      val consts = NameSpace.merge_tables eq_snd (consts1, consts2)
    20.8 +      val consts = NameSpace.merge_tables (eq_snd (op =)) (consts1, consts2)
    20.9          handle Symtab.DUPS cs => err_dup_consts cs;
   20.10        val constraints = Symtab.merge (op =) (constraints1, constraints2)
   20.11          handle Symtab.DUPS cs => err_inconsistent_constraints cs;
    21.1 --- a/src/Pure/tactic.ML	Tue Sep 20 08:20:22 2005 +0200
    21.2 +++ b/src/Pure/tactic.ML	Tue Sep 20 08:21:49 2005 +0200
    21.3 @@ -573,9 +573,9 @@
    21.4  (*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
    21.5    Returns longest lhs first to avoid folding its subexpressions.*)
    21.6  fun sort_lhs_depths defs =
    21.7 -  let val keylist = make_keylist (term_depth o lhs_of_thm) defs
    21.8 +  let val keylist = AList.make (term_depth o lhs_of_thm) defs
    21.9        val keys = distinct (sort (rev_order o int_ord) (map #2 keylist))
   21.10 -  in  map (keyfilter keylist) keys  end;
   21.11 +  in map (AList.find (op =) keylist) keys end;
   21.12  
   21.13  val rev_defs = sort_lhs_depths o map symmetric;
   21.14  
    22.1 --- a/src/Pure/theory.ML	Tue Sep 20 08:20:22 2005 +0200
    22.2 +++ b/src/Pure/theory.ML	Tue Sep 20 08:21:49 2005 +0200
    22.3 @@ -120,7 +120,7 @@
    22.4  
    22.5        val axioms = NameSpace.empty_table;
    22.6        val defs = Defs.merge pp defs1 defs2;
    22.7 -      val oracles = NameSpace.merge_tables eq_snd (oracles1, oracles2)
    22.8 +      val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
    22.9          handle Symtab.DUPS dups => err_dup_oras dups;
   22.10      in make_thy (axioms, defs, oracles) end;
   22.11  
    23.1 --- a/src/Pure/type.ML	Tue Sep 20 08:20:22 2005 +0200
    23.2 +++ b/src/Pure/type.ML	Tue Sep 20 08:21:49 2005 +0200
    23.3 @@ -632,7 +632,7 @@
    23.4  fun add_nonterminals naming = change_types o fold (new_decl naming) o map (rpair Nonterminal);
    23.5  
    23.6  fun merge_types (types1, types2) =
    23.7 -  NameSpace.merge_tables Library.eq_snd (types1, types2) handle Symtab.DUPS (d :: _) =>
    23.8 +  NameSpace.merge_tables (Library.eq_snd (op =)) (types1, types2) handle Symtab.DUPS (d :: _) =>
    23.9      err_in_decls d (the_decl types1 d) (the_decl types2 d);
   23.10  
   23.11  end;
    24.1 --- a/src/Pure/type_infer.ML	Tue Sep 20 08:20:22 2005 +0200
    24.2 +++ b/src/Pure/type_infer.ML	Tue Sep 20 08:21:49 2005 +0200
    24.3 @@ -452,7 +452,7 @@
    24.4        xi = xi' andalso Type.eq_sort tsig (S, S');
    24.5  
    24.6      val env = gen_distinct eq (map (apsnd map_sort) raw_env);
    24.7 -    val _ = (case gen_duplicates eq_fst env of [] => ()
    24.8 +    val _ = (case gen_duplicates (eq_fst (op =)) env of [] => ()
    24.9        | dups => error ("Inconsistent sort constraints for type variable(s) "
   24.10            ^ commas_quote (map (Syntax.string_of_vname' o fst) dups)));
   24.11