src/Pure/Isar/isar_cmd.ML

 (* goals *)
 
 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 *)
 
 fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));

       Graph.fold (cons o entry) classes []
       |> sort (int_ord o pairself #1) |> map #2;
   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 *)
 
 fun unused_thms opt_range = Toplevel.keep (fn state =>

 (* print theorems, terms, types etc. *)
 
 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
     (case arg of
       NONE =>

           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 state args)));
+          (Proof.get_thmss_cmd state args)));
 
 fun string_of_prop state s =
   let
     val ctxt = Proof.context_of state;
     val prop = Syntax.read_prop ctxt s;