--- 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;