src/Pure/Tools/named_thms.ML
changeset 26397 df68e8dfd0e3
parent 26363 9d95309f8069
child 26724 ff6ff3a9010e
     1.1 --- a/src/Pure/Tools/named_thms.ML	Tue Mar 25 21:01:02 2008 +0100
     1.2 +++ b/src/Pure/Tools/named_thms.ML	Tue Mar 25 21:01:03 2008 +0100
     1.3 @@ -39,7 +39,8 @@
     1.4  val del = Thm.declaration_attribute del_thm;
     1.5  
     1.6  val setup =
     1.7 -  Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)];
     1.8 +  Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)] #>
     1.9 +  PureThy.add_thms_dynamic (name, Data.get);
    1.10  
    1.11  val _ =
    1.12    OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description)