src/Pure/Proof/extraction.ML
changeset 22662 3e492ba59355
parent 22596 d0d2af4db18f
child 22675 acf10be7dcca
     1.1 --- a/src/Pure/Proof/extraction.ML	Fri Apr 13 15:43:25 2007 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Fri Apr 13 16:40:16 2007 +0200
     1.3 @@ -206,8 +206,8 @@
     1.4       typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
     1.5       types = merge_alists types1 types2,
     1.6       realizers = Symtab.merge_list (gen_eq_set (op =) o pairself #1) (realizers1, realizers2),
     1.7 -     defs = gen_merge_lists Thm.eq_thm defs1 defs2,
     1.8 -     expand = merge_lists expand1 expand2,
     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  
    1.13    fun print _ _ = ();