# HG changeset patch
# User wenzelm
# Date 938356701 -7200
# Node ID 1acbed762fc6ae4d34a5bb983de1eb025c40d528
# Parent  8069542cba828d84c32a910d709296b1f1d6b0ff
added print_thms_containing;

diff -r 8069542cba82 -r 1acbed762fc6 src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Sat Sep 25 13:25:16 1999 +0200
+++ b/src/Pure/Thy/thm_database.ML	Sun Sep 26 16:38:21 1999 +0200
@@ -29,6 +29,7 @@
   val ml_store_thm: string * thm -> unit
   val ml_store_thms: string * thm list -> unit
   val is_ml_identifier: string -> bool
+  val print_thms_containing: theory -> xstring list -> unit
 end;
 
 structure ThmDatabase: THM_DATABASE =
@@ -93,14 +94,21 @@
 (** retrieve theorems **)
 
 (*get theorems that contain all of given constants*)
-fun thms_containing raw_consts =
-  let
-    val sign = sign_of_thm (topthm ());
-    val consts = map (Sign.intern_const sign) raw_consts;
-    val thy = ThyInfo.theory_of_sign sign;
+fun thms_containing_thy thy raw_consts =
+  let val consts = map (Sign.intern_const (Theory.sign_of thy)) raw_consts;
   in PureThy.thms_containing thy consts end
   handle THEORY (msg,_) => error msg;
 
+fun thms_containing cs =
+  thms_containing_thy (ThyInfo.theory_of_sign (Thm.sign_of_thm (Goals.topthm ()))) cs;
+
+fun prt_thm (a, th) =
+  Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
+    Display.pretty_thm_no_quote (#1 (Drule.freeze_thaw th))];
+
+fun print_thms_containing thy cs =
+  Pretty.writeln (Pretty.blk (0, Pretty.fbreaks (map prt_thm (thms_containing_thy thy cs))));
+
 
 (*top_const: main constant, ignoring Trueprop*)
 fun top_const (_ $ t) = (case head_of t of Const (c, _) => Some c | _ => None)