diff -r 5cd130251825 -r 3e58c7cb5a73 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Sun Nov 11 14:00:05 2007 +0100
+++ b/src/Pure/consts.ML	Sun Nov 11 14:00:08 2007 +0100
@@ -288,7 +288,7 @@
         val decls' = decls
           |> extend_decls naming (c, ((decl, SOME abbr), serial ()));
         val rev_abbrevs' = rev_abbrevs
-          |> fold (curry Symtab.update_list mode) (rev_abbrev lhs rhs);
+          |> fold (curry Symtab.cons_list mode) (rev_abbrev lhs rhs);
       in (decls', constraints, rev_abbrevs') end)
     |> pair (lhs, rhs)
   end;
@@ -297,7 +297,7 @@
   let
     val (T, rhs) = the_abbreviation consts c;
     val rev_abbrevs' = rev_abbrevs
-      |> fold (curry Symtab.update_list mode) (rev_abbrev (Const (c, T)) rhs);
+      |> fold (curry Symtab.cons_list mode) (rev_abbrev (Const (c, T)) rhs);
   in (decls, constraints, rev_abbrevs') end);
 
 end;