NamedThmsFun: removed obsolete print command -- facts are accesible via dynamic name;
authorwenzelm
Sat Apr 19 12:04:17 2008 +0200 (2008-04-19)
changeset 26724ff6ff3a9010e
parent 26723 3e4bb1ca9a74
child 26725 4d9ca7a6b586
NamedThmsFun: removed obsolete print command -- facts are accesible via dynamic name;
NEWS
src/Pure/Tools/named_thms.ML
     1.1 --- a/NEWS	Fri Apr 18 23:58:04 2008 +0200
     1.2 +++ b/NEWS	Sat Apr 19 12:04:17 2008 +0200
     1.3 @@ -246,7 +246,7 @@
     1.4  *** ML ***
     1.5  
     1.6  * Functor NamedThmsFun: data is available to the user as dynamic fact
     1.7 -(of the same name).
     1.8 +(of the same name).  Removed obsolete print command.
     1.9  
    1.10  * Removed obsolete "use_legacy_bindings" function.  INCOMPATIBILITY.
    1.11  
     2.1 --- a/src/Pure/Tools/named_thms.ML	Fri Apr 18 23:58:04 2008 +0200
     2.2 +++ b/src/Pure/Tools/named_thms.ML	Sat Apr 19 12:04:17 2008 +0200
     2.3 @@ -8,7 +8,6 @@
     2.4  signature NAMED_THMS =
     2.5  sig
     2.6    val get: Proof.context -> thm list
     2.7 -  val pretty: Proof.context -> Pretty.T
     2.8    val add_thm: thm -> Context.generic -> Context.generic
     2.9    val del_thm: thm -> Context.generic -> Context.generic
    2.10    val add: attribute
    2.11 @@ -29,9 +28,6 @@
    2.12  
    2.13  val get = Data.get o Context.Proof;
    2.14  
    2.15 -fun pretty ctxt =
    2.16 -  Pretty.big_list (description ^ ":") (map (ProofContext.pretty_thm ctxt) (get ctxt));
    2.17 -
    2.18  val add_thm = Data.map o Thm.add_thm;
    2.19  val del_thm = Data.map o Thm.del_thm;
    2.20  
    2.21 @@ -42,10 +38,4 @@
    2.22    Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)] #>
    2.23    PureThy.add_thms_dynamic (name, Data.get);
    2.24  
    2.25 -val _ =
    2.26 -  OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description)
    2.27 -    OuterKeyword.diag
    2.28 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    2.29 -      Toplevel.keep (Pretty.writeln o pretty o Toplevel.context_of)));
    2.30 -
    2.31  end;