# HG changeset patch
# User wenzelm
# Date 1126642776 -7200
# Node ID 5bc9f8c81d586c5260ff11e10386bfb3a2d7f3de
# Parent  f7f2f56fcc28a3726c3fb2a6aa0aebe14df6ac52
Proof.get_thmss;

diff -r f7f2f56fcc28 -r 5bc9f8c81d58 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Sep 13 22:19:35 2005 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Sep 13 22:19:36 2005 +0200
@@ -268,7 +268,7 @@
 (* retrieve theorems *)
 
 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
-  ThmDeps.thm_deps (IsarThy.get_thmss args (Toplevel.enter_forward_proof state)));
+  ThmDeps.thm_deps (Proof.get_thmss (Toplevel.enter_forward_proof state) args));
 
 fun find_theorems (opt_lim, spec) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   let
@@ -295,7 +295,7 @@
 
 fun string_of_thms state ms args = with_modes ms (fn () =>
   Pretty.string_of (ProofContext.pretty_thms (Proof.context_of state)
-    (IsarThy.get_thmss args state)));
+    (Proof.get_thmss state args)));
 
 fun string_of_prfs full state ms arg = with_modes ms (fn () =>
   Pretty.string_of (case arg of
@@ -311,7 +311,7 @@
         end
     | SOME args => Pretty.chunks
         (map (ProofContext.pretty_proof_of (Proof.context_of state) full)
-          (IsarThy.get_thmss args state))));
+          (Proof.get_thmss state args))));
 
 fun string_of_prop state ms s =
   let