--- 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;