# HG changeset patch
# User wenzelm
# Date 1116773470 -7200
# Node ID 96a9bf7ac18df0bafa60b9a37392b04e601fc4a9
# Parent  ff83bc2151bf3397dfaa7a171f448f9b377125df
FindTheorems.print_theorems;

diff -r ff83bc2151bf -r 96a9bf7ac18d src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Sun May 22 16:51:09 2005 +0200
+++ b/src/Pure/proof_general.ML	Sun May 22 16:51:10 2005 +0200
@@ -371,13 +371,12 @@
 
 end
 
+
 (* misc commands for ProofGeneral/isa *)
 
-(* PG/isa mode does not go through the Isar parser, hence we 
-   interpret everything as term pattern only *)
 fun thms_containing ss =
-  ProofContext.print_thms_containing (ProofContext.init (the_context ())) NONE NONE 
-    (map (fn s => (true, ProofContext.Pattern s)) ss);
+  FindTheorems.print_theorems (ProofContext.init (the_context ())) NONE NONE 
+    (map (fn s => (true, FindTheorems.Pattern s)) ss);
 
 val welcome = priority o Session.welcome;
 val help = welcome;