src/Pure/Proof/extraction.ML
changeset 18921 f47c46d7d654
parent 18728 6790126ab5f6
child 18928 042608ffa2ec
     1.1 --- a/src/Pure/Proof/extraction.ML	Fri Feb 03 17:08:03 2006 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Fri Feb 03 23:12:28 2006 +0100
     1.3 @@ -374,7 +374,7 @@
     1.4           typeof_eqns = add_rule (([],
     1.5             Logic.dest_equals (prop_of (Drule.abs_def thm))), typeof_eqns),
     1.6           types = types,
     1.7 -         realizers = realizers, defs = gen_ins eq_thm (thm, defs),
     1.8 +         realizers = realizers, defs = insert eq_thm thm defs,
     1.9           expand = expand, prep = prep}
    1.10        else
    1.11          {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,