src/Pure/Proof/extraction.ML
changeset 25389 3e58c7cb5a73
parent 24867 e5b55d7be9bb
child 26336 a0e2b706ce73
     1.1 --- a/src/Pure/Proof/extraction.ML	Sun Nov 11 14:00:05 2007 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sun Nov 11 14:00:08 2007 +0100
     1.3 @@ -294,7 +294,7 @@
     1.4    in
     1.5      ExtractionData.put
     1.6        {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
     1.7 -       realizers = fold (Symtab.update_list o prep_rlz thy) rs realizers,
     1.8 +       realizers = fold (Symtab.cons_list o prep_rlz thy) rs realizers,
     1.9         defs = defs, expand = expand, prep = prep} thy
    1.10    end
    1.11