# HG changeset patch
# User wenzelm
# Date 1139256000 -3600
# Node ID 9881ff995ff573fa17875a944f48af7363b9b296
# Parent  9bf24144404f273ab38618ac372170ed2ba02e7d
adapted Consts.dest;

diff -r 9bf24144404f -r 9881ff995ff5 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Mon Feb 06 20:59:59 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Mon Feb 06 21:00:00 2006 +0100
@@ -1069,7 +1069,7 @@
           |> fold (Symtab.fold (Symtab.remove (K true)) o get) (Theory.parents_of thy)
           |> Symtab.keys;
         val names = own_tables (#2 o #types o Type.rep_tsig o Sign.tsig_of)
-          @ own_tables (#2 o #declarations o Consts.dest o #consts o Sign.rep_sg);
+          @ own_tables (#2 o #constants o Consts.dest o #consts o Sign.rep_sg);
         fun diff names =
           fold (fn name =>
             if is_prefix (op =) (NameSpace.unpack thyname) (NameSpace.unpack name)