--- a/src/Pure/Tools/named_thms.ML Tue Mar 25 21:01:02 2008 +0100
+++ b/src/Pure/Tools/named_thms.ML Tue Mar 25 21:01:03 2008 +0100
@@ -39,7 +39,8 @@
val del = Thm.declaration_attribute del_thm;
val setup =
- Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)];
+ Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)] #>
+ PureThy.add_thms_dynamic (name, Data.get);
val _ =
OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description)