# HG changeset patch
# User wenzelm
# Date 938356730 -7200
# Node ID c803ba5347fdd479d6ec8eb0fb86915531301c66
# Parent  1acbed762fc6ae4d34a5bb983de1eb025c40d528
ThmDatabase.print_thms_containing;

diff -r 1acbed762fc6 -r c803ba5347fd src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Sun Sep 26 16:38:21 1999 +0200
+++ b/src/Pure/Interface/proof_general.ML	Sun Sep 26 16:38:50 1999 +0200
@@ -166,14 +166,7 @@
 
 (* some top-level commands for ProofGeneral/isa *)
 
-fun prt_thm (a, th) =
-  Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
-    Display.pretty_thm_no_quote (#1 (Drule.freeze_thaw th))];
-
-fun thms_containing cs =
-  Pretty.blk (0, Pretty.fbreaks (map prt_thm (ThmDatabase.thms_containing cs)))
-  |> Pretty.writeln;
-
+fun thms_containing cs = ThmDatabase.print_thms_containing (the_context ()) cs;
 
 val help = writeln o Session.welcome;
 val show_context = Context.the_context;