# HG changeset patch
# User wenzelm
# Date 1206475263 -3600
# Node ID df68e8dfd0e3c75975635adde5242001a0723c0f
# Parent  e44c5a1a47bd3e0c5498b2786315fbb6b51c54bd
add dynamic fact binding;

diff -r e44c5a1a47bd -r df68e8dfd0e3 src/Pure/Tools/named_thms.ML
--- 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)