src/Pure/Isar/isar_cmd.ML

--- a/src/Pure/Isar/isar_cmd.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -219,10 +219,10 @@
 fun goal opt_chain goal stmt int =
   opt_chain #> goal NONE (K I) stmt int;
 
-val have = goal I Proof.have;
-val hence = goal Proof.chain Proof.have;
-val show = goal I Proof.show;
-val thus = goal Proof.chain Proof.show;
+val have = goal I Proof.have_cmd;
+val hence = goal Proof.chain Proof.have_cmd;
+val show = goal I Proof.show_cmd;
+val thus = goal Proof.chain Proof.show_cmd;
 
 
 (* local endings *)
@@ -403,7 +403,7 @@
   in Present.display_graph gr end);
 
 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
-  Thm_Deps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
+  Thm_Deps.thm_deps (Proof.get_thmss_cmd (Toplevel.enter_proof_body state) args));
 
 
 (* find unused theorems *)
@@ -437,12 +437,12 @@
 local
 
 fun string_of_stmts state args =
-  Proof.get_thmss state args
+  Proof.get_thmss_cmd state args
   |> map (Element.pretty_statement (Proof.context_of state) 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 state args));
+  Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss_cmd state args));
 
 fun string_of_prfs full state arg =
   Pretty.string_of
@@ -460,7 +460,7 @@
         end
     | SOME args => Pretty.chunks
         (map (Proof_Syntax.pretty_proof_of (Proof.context_of state) full)
-          (Proof.get_thmss state args)));
+          (Proof.get_thmss_cmd state args)));
 
 fun string_of_prop state s =
   let