src/Pure/Isar/locale.ML
changeset 17496 26535df536ae
parent 17485 c39871c52977
child 17756 d4a35f82fbb4
     1.1 --- a/src/Pure/Isar/locale.ML	Tue Sep 20 08:20:22 2005 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Tue Sep 20 08:21:49 2005 +0200
     1.3 @@ -372,7 +372,7 @@
     1.4    fun join_locs _ ({predicate, import, elems, params, regs}: locale,
     1.5        {elems = elems', regs = regs', ...}: locale) =
     1.6      SOME {predicate = predicate, import = import,
     1.7 -      elems = gen_merge_lists eq_snd elems elems',
     1.8 +      elems = gen_merge_lists (eq_snd (op =)) elems elems',
     1.9        params = params,
    1.10        regs = merge_alists regs regs'};
    1.11    fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
    1.12 @@ -770,10 +770,10 @@
    1.13      val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (List.mapPartial I Vs));
    1.14    in map (Option.map (Envir.norm_type unifier')) Vs end;
    1.15  
    1.16 -fun params_of elemss = gen_distinct eq_fst (List.concat (map (snd o fst) elemss));
    1.17 -fun params_of' elemss = gen_distinct eq_fst (List.concat (map (snd o fst o fst) elemss));
    1.18 +fun params_of elemss = gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss));
    1.19 +fun params_of' elemss = gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst o fst) elemss));
    1.20  fun params_syn_of syn elemss =
    1.21 -  gen_distinct eq_fst (List.concat (map (snd o fst) elemss)) |>
    1.22 +  gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss)) |>
    1.23      map (apfst (fn x => (x, valOf (Symtab.lookup syn x))));
    1.24  
    1.25  
    1.26 @@ -843,7 +843,7 @@
    1.27      val (unifier, _) = Library.foldl unify_list
    1.28        ((Vartab.empty, maxidx), map #2 (Symtab.dest (Symtab.make_multi parms)));
    1.29  
    1.30 -    val parms' = map (apsnd (Envir.norm_type unifier)) (gen_distinct eq_fst parms);
    1.31 +    val parms' = map (apsnd (Envir.norm_type unifier)) (gen_distinct (eq_fst (op =)) parms);
    1.32      val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
    1.33  
    1.34      fun inst_parms (i, ps) =
    1.35 @@ -939,7 +939,7 @@
    1.36              (* propagate parameter types, to keep them consistent *)
    1.37            val regs' = map (fn ((name, ps), ths) =>
    1.38                ((name, map (rename ren) ps), ths)) regs;
    1.39 -          val new_regs = gen_rems eq_fst (regs', ids);
    1.40 +          val new_regs = gen_rems (eq_fst (op =)) (regs', ids);
    1.41            val new_ids = map fst new_regs;
    1.42            val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) ps) p)))) new_ids;
    1.43  
    1.44 @@ -993,7 +993,7 @@
    1.45              val ren = renaming xs parms'
    1.46                handle ERROR_MESSAGE msg => err_in_locale' ctxt msg ids';
    1.47  
    1.48 -            val ids'' = gen_distinct eq_fst (map (rename_parms top ren) ids');
    1.49 +            val ids'' = gen_distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
    1.50              val parms'' = distinct (List.concat (map (#2 o #1) ids''));
    1.51              val syn'' = syn' |> Symtab.dest |> map (rename_var ren) |>
    1.52                    Symtab.make;
    1.53 @@ -1037,7 +1037,7 @@
    1.54  
    1.55      (* compute identifiers and syntax, merge with previous ones *)
    1.56      val (ids, _, syn) = identify true expr;
    1.57 -    val idents = gen_rems eq_fst (ids, prev_idents);
    1.58 +    val idents = gen_rems (eq_fst (op =)) (ids, prev_idents);
    1.59      val syntax = merge_syntax ctxt ids (syn, prev_syntax);
    1.60      (* add types to params, check for unique params and unify them *)
    1.61      val raw_elemss = unique_parms ctxt (map (eval syntax) idents);