# HG changeset patch
# User wenzelm
# Date 1025617555 -7200
# Node ID 8a722689a1c96f92a57fe359831ba6e885cb2d22
# Parent  b62514fcbcab5ca977b7f1886b770cfe26d7ba8d
removed thms_containing (see pure_thy.ML and proof_context.ML);

diff -r b62514fcbcab -r 8a722689a1c9 src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Tue Jul 02 15:44:04 2002 +0200
+++ b/src/Pure/Thy/thm_database.ML	Tue Jul 02 15:45:55 2002 +0200
@@ -3,7 +3,7 @@
     Author:     Markus Wenzel, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Interface to thm database (see also Pure/pure_thy.ML).
+Interface to thm database.
 *)
 
 signature BASIC_THM_DATABASE =
@@ -20,8 +20,6 @@
   val ml_store_thms: string * thm list -> unit
   val is_ml_identifier: string -> bool
   val ml_reserved: string list
-  val thms_containing: theory -> string list -> (string * thm) list
-  val print_thms_containing: theory -> term list -> unit
 end;
 
 structure ThmDatabase: THM_DATABASE =
@@ -29,7 +27,7 @@
 
 (** store theorems **)
 
-(* store in theory and generate HTML *)
+(* store in theory and perform presentation *)
 
 fun store_thm (name, thm) =
   let val thm' = hd (PureThy.smart_store_thms (name, [thm]))
@@ -65,7 +63,8 @@
 fun ml_store_thm (name, thm) =
   let val thm' = store_thm (name, thm) in
     if warn_ml name then ()
-    else (qed_thms := [thm']; use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);"))
+    else (qed_thms := [thm'];
+      use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);"))
   end;
 
 fun ml_store_thms (name, thms) =
@@ -75,31 +74,6 @@
   end;
 
 
-
-(** retrieve theorems **)
-
-fun thms_containing thy consts = PureThy.thms_containing thy consts
-  handle THEORY (msg, _) => error msg | THM (msg, _, _) => error msg;
-
-fun print_thms_containing thy ts =
-  let
-    val prt_const =
-      Pretty.quote o Pretty.str o Sign.cond_extern (Theory.sign_of thy) Sign.constK;
-    fun prt_thm (a, th) = Pretty.block [Pretty.str (a ^ ":"),
-      Pretty.brk 1, Display.pretty_thm_no_quote (#1 (Drule.freeze_thaw th))];
-
-    val cs = foldr Term.add_term_consts (ts, []);
-    val header =
-      if Library.null cs then []
-      else [Pretty.block (Pretty.breaks (Pretty.str "theorems containing constants:" ::
-          map prt_const cs)), Pretty.str ""];
-  in
-    if Library.null cs andalso not (Library.null ts) then
-      warning "thms_containing: no constants in specification"
-    else (header @ map prt_thm (thms_containing thy cs)) |> Pretty.chunks |> Pretty.writeln
-  end;
-
-
 end;
 
 structure BasicThmDatabase: BASIC_THM_DATABASE = ThmDatabase;