# HG changeset patch
# User wenzelm
# Date 1208599457 -7200
# Node ID ff6ff3a9010e10bca856606817010374f1ac7fbe
# Parent  3e4bb1ca9a74ae34f707868cb7fd356d9cabe536
NamedThmsFun: removed obsolete print command -- facts are accesible via dynamic name;

diff -r 3e4bb1ca9a74 -r ff6ff3a9010e NEWS
--- a/NEWS	Fri Apr 18 23:58:04 2008 +0200
+++ b/NEWS	Sat Apr 19 12:04:17 2008 +0200
@@ -246,7 +246,7 @@
 *** ML ***
 
 * Functor NamedThmsFun: data is available to the user as dynamic fact
-(of the same name).
+(of the same name).  Removed obsolete print command.
 
 * Removed obsolete "use_legacy_bindings" function.  INCOMPATIBILITY.
 
diff -r 3e4bb1ca9a74 -r ff6ff3a9010e src/Pure/Tools/named_thms.ML
--- a/src/Pure/Tools/named_thms.ML	Fri Apr 18 23:58:04 2008 +0200
+++ b/src/Pure/Tools/named_thms.ML	Sat Apr 19 12:04:17 2008 +0200
@@ -8,7 +8,6 @@
 signature NAMED_THMS =
 sig
   val get: Proof.context -> thm list
-  val pretty: Proof.context -> Pretty.T
   val add_thm: thm -> Context.generic -> Context.generic
   val del_thm: thm -> Context.generic -> Context.generic
   val add: attribute
@@ -29,9 +28,6 @@
 
 val get = Data.get o Context.Proof;
 
-fun pretty ctxt =
-  Pretty.big_list (description ^ ":") (map (ProofContext.pretty_thm ctxt) (get ctxt));
-
 val add_thm = Data.map o Thm.add_thm;
 val del_thm = Data.map o Thm.del_thm;
 
@@ -42,10 +38,4 @@
   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)
-    OuterKeyword.diag
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
-      Toplevel.keep (Pretty.writeln o pretty o Toplevel.context_of)));
-
 end;