--- a/src/Pure/Isar/isar_cmd.ML Sun Sep 26 16:44:03 1999 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Sun Sep 26 16:45:00 1999 +0200
@@ -38,6 +38,7 @@
val print_theorems: Toplevel.transition -> Toplevel.transition
val print_attributes: Toplevel.transition -> Toplevel.transition
val print_methods: Toplevel.transition -> Toplevel.transition
+ val print_thms_containing: xstring list -> Toplevel.transition -> Toplevel.transition
val print_binds: Toplevel.transition -> Toplevel.transition
val print_lthms: Toplevel.transition -> Toplevel.transition
val print_thms: (string * Args.src list) list -> Toplevel.transition -> Toplevel.transition
@@ -96,11 +97,11 @@
Context.setmp (try Toplevel.theory_of state) ThyInfo.use name);
(*passes changes of theory context*)
-val use_mltext_theory = Toplevel.theory o IsarThy.use_mltext_theory;
+val use_mltext_theory = Toplevel.theory' o IsarThy.use_mltext_theory;
(*ignore result theory context*)
-fun use_mltext txt = Toplevel.keep (fn state =>
- (IsarThy.use_mltext txt (try Toplevel.theory_of state); ()));
+fun use_mltext txt = Toplevel.keep' (fn verb => fn state =>
+ (IsarThy.use_mltext txt verb (try Toplevel.theory_of state)));
(*Note: commit is dynamically bound*)
val use_commit = use_mltext "commit();";
@@ -137,6 +138,9 @@
val print_attributes = Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
val print_methods = Toplevel.keep (Method.print_methods o Toplevel.theory_of);
+fun print_thms_containing cs = Toplevel.keep (fn state =>
+ ThmDatabase.print_thms_containing (Toplevel.theory_of state) cs);
+
(* print proof context contents *)