# HG changeset patch
# User wenzelm
# Date 1025617093 -7200
# Node ID 6fea54cf6fb501abaf61ae5c9b73ccedd2da6107
# Parent  eb0b565909a0021306dd1103bdfffb824623cc3a
ProofContext.print_thms_containing;

diff -r eb0b565909a0 -r 6fea54cf6fb5 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Jul 02 15:37:49 2002 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Jul 02 15:38:13 2002 +0200
@@ -225,8 +225,8 @@
 val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations;
 
 fun print_thms_containing ss = Toplevel.unknown_theory o Toplevel.keep (fn state =>
-  ThmDatabase.print_thms_containing (Toplevel.theory_of state)
-    (map (ProofContext.read_term (Toplevel.context_of state)) ss));
+  ProofContext.print_thms_containing
+    (Toplevel.node_case ProofContext.init Proof.context_of state) ss);
 
 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   ThmDeps.thm_deps (IsarThy.get_thmss args (Toplevel.enter_forward_proof state)));
diff -r eb0b565909a0 -r 6fea54cf6fb5 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Tue Jul 02 15:37:49 2002 +0200
+++ b/src/Pure/proof_general.ML	Tue Jul 02 15:38:13 2002 +0200
@@ -220,10 +220,7 @@
 (* misc commands for ProofGeneral/isa *)
 
 fun thms_containing ss =
-  let
-    val thy = the_context ();
-    fun read_term s = Thm.term_of (Thm.read_cterm (Theory.sign_of thy) (s, TypeInfer.logicT));
-  in ThmDatabase.print_thms_containing thy (map read_term ss) end;
+  ProofContext.print_thms_containing (ProofContext.init (the_context ())) ss;
 
 val welcome = priority o Session.welcome;
 val help = welcome;