diff -r e98236e5068b -r 6e72f31999ac src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Aug 11 17:24:57 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Aug 11 17:29:54 2010 +0200
@@ -416,7 +416,7 @@
 
 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   Thm_Deps.thm_deps (Toplevel.theory_of state)
-    (Proof.get_thmss_cmd (Toplevel.enter_proof_body state) args));
+    (Attrib.eval_thms (Toplevel.context_of state) args));
 
 
 (* find unused theorems *)
@@ -450,20 +450,20 @@
 
 local
 
-fun string_of_stmts state args =
-  Proof.get_thmss_cmd state args
-  |> map (Element.pretty_statement (Proof.context_of state) Thm.theoremK)
+fun string_of_stmts ctxt args =
+  Attrib.eval_thms ctxt args
+  |> map (Element.pretty_statement ctxt Thm.theoremK)
   |> Pretty.chunks2 |> Pretty.string_of;
 
-fun string_of_thms state args =
-  Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss_cmd state args));
+fun string_of_thms ctxt args =
+  Pretty.string_of (Display.pretty_thms ctxt (Attrib.eval_thms ctxt args));
 
 fun string_of_prfs full state arg =
   Pretty.string_of
     (case arg of
       NONE =>
         let
-          val {context = ctxt, goal = thm} = Proof.simple_goal state;
+          val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state);
           val thy = ProofContext.theory_of ctxt;
           val prf = Thm.proof_of thm;
           val prop = Thm.full_prop_of thm;
@@ -472,20 +472,19 @@
           Proof_Syntax.pretty_proof ctxt
             (if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
         end
-    | SOME args => Pretty.chunks
-        (map (Proof_Syntax.pretty_proof_of (Proof.context_of state) full)
-          (Proof.get_thmss_cmd state args)));
+    | SOME srcs =>
+        let val ctxt = Toplevel.context_of state
+        in map (Proof_Syntax.pretty_proof_of ctxt full) (Attrib.eval_thms ctxt srcs) end
+        |> Pretty.chunks);
 
-fun string_of_prop state s =
+fun string_of_prop ctxt s =
   let
-    val ctxt = Proof.context_of state;
     val prop = Syntax.read_prop ctxt s;
     val ctxt' = Variable.auto_fixes prop ctxt;
   in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end;
 
-fun string_of_term state s =
+fun string_of_term ctxt s =
   let
-    val ctxt = Proof.context_of state;
     val t = Syntax.read_term ctxt s;
     val T = Term.type_of t;
     val ctxt' = Variable.auto_fixes t ctxt;
@@ -495,24 +494,21 @@
         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)])
   end;
 
-fun string_of_type state s =
-  let
-    val ctxt = Proof.context_of state;
-    val T = Syntax.read_typ ctxt s;
+fun string_of_type ctxt s =
+  let val T = Syntax.read_typ ctxt s
   in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end;
 
 fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
-  Print_Mode.with_modes modes (fn () =>
-    writeln (string_of (Toplevel.enter_proof_body state) arg)) ());
+  Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ());
 
 in
 
-val print_stmts = print_item string_of_stmts;
-val print_thms = print_item string_of_thms;
+val print_stmts = print_item (string_of_stmts o Toplevel.context_of);
+val print_thms = print_item (string_of_thms o Toplevel.context_of);
 val print_prfs = print_item o string_of_prfs;
-val print_prop = print_item string_of_prop;
-val print_term = print_item string_of_term;
-val print_type = print_item string_of_type;
+val print_prop = print_item (string_of_prop o Toplevel.context_of);
+val print_term = print_item (string_of_term o Toplevel.context_of);
+val print_type = print_item (string_of_type o Toplevel.context_of);
 
 end;