src/Pure/Proof/extraction.ML
changeset 33038 8f9594c31de4
parent 32784 1a5dde5079ac
child 33245 65232054ffd0
     1.1 --- a/src/Pure/Proof/extraction.ML	Tue Oct 20 16:13:01 2009 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Wed Oct 21 08:14:38 2009 +0200
     1.3 @@ -198,7 +198,7 @@
     1.4      {realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
     1.5       typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
     1.6       types = AList.merge (op =) (K true) (types1, types2),
     1.7 -     realizers = Symtab.merge_list (gen_eq_set (op =) o pairself #1) (realizers1, realizers2),
     1.8 +     realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2),
     1.9       defs = Library.merge Thm.eq_thm (defs1, defs2),
    1.10       expand = Library.merge (op =) (expand1, expand2),
    1.11       prep = (case prep1 of NONE => prep2 | _ => prep1)};
    1.12 @@ -468,7 +468,7 @@
    1.13  
    1.14        in List.foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
    1.15  
    1.16 -    fun find (vs: string list) = Option.map snd o find_first (curry (gen_eq_set (op =)) vs o fst);
    1.17 +    fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
    1.18      fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
    1.19  
    1.20      fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw