src/Pure/Proof/extraction.ML
changeset 19305 5c16895d548b
parent 18956 c050ae1f8f52
child 19391 4812d28c90a6
     1.1 --- a/src/Pure/Proof/extraction.ML	Tue Mar 21 12:18:13 2006 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Tue Mar 21 12:18:15 2006 +0100
     1.3 @@ -84,7 +84,7 @@
     1.4  
     1.5  fun merge_rules
     1.6    ({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) =
     1.7 -  foldr add_rule {next = next, rs = rs1, net = net} (rs2 \\ rs1);
     1.8 +  foldr add_rule {next = next, rs = rs1, net = net} (subtract (op =) rs1 rs2);
     1.9  
    1.10  fun condrew thy rules procs =
    1.11    let
    1.12 @@ -205,7 +205,7 @@
    1.13      {realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
    1.14       typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
    1.15       types = merge_alists types1 types2,
    1.16 -     realizers = Symtab.merge_list (eq_set o pairself #1) (realizers1, realizers2),
    1.17 +     realizers = Symtab.merge_list (gen_eq_set (op =) o pairself #1) (realizers1, realizers2),
    1.18       defs = gen_merge_lists eq_thm defs1 defs2,
    1.19       expand = merge_lists expand1 expand2,
    1.20       prep = (case prep1 of NONE => prep2 | _ => prep1)};
    1.21 @@ -483,7 +483,7 @@
    1.22  
    1.23        in foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
    1.24  
    1.25 -    fun find vs = Option.map snd o find_first (curry eq_set vs o fst);
    1.26 +    fun find vs = Option.map snd o find_first (curry (gen_eq_set (op =)) vs o fst);
    1.27      fun find' s = map snd o List.filter (equal s o fst)
    1.28  
    1.29      fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw