diff -r 5cd130251825 -r 3e58c7cb5a73 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sun Nov 11 14:00:05 2007 +0100
+++ b/src/Pure/Proof/extraction.ML	Sun Nov 11 14:00:08 2007 +0100
@@ -294,7 +294,7 @@
   in
     ExtractionData.put
       {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
-       realizers = fold (Symtab.update_list o prep_rlz thy) rs realizers,
+       realizers = fold (Symtab.cons_list o prep_rlz thy) rs realizers,
        defs = defs, expand = expand, prep = prep} thy
   end