src/Pure/Isar/isar_cmd.ML

   val undo_theory: Toplevel.transition -> Toplevel.transition
   val undo: Toplevel.transition -> Toplevel.transition
   val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
   val kill: Toplevel.transition -> Toplevel.transition
   val back: Toplevel.transition -> Toplevel.transition
-  val use: Path.T -> Toplevel.transition -> Toplevel.transition
-  val use_mltext_theory: string * Position.T -> Toplevel.transition -> Toplevel.transition
-  val use_mltext: bool -> string * Position.T -> Toplevel.transition -> Toplevel.transition
-  val use_commit: Toplevel.transition -> Toplevel.transition
+  val ml_diag: bool -> string * Position.T -> Toplevel.transition -> Toplevel.transition
   val nested_command: Markup.property list -> string * Position.T -> Toplevel.transition
   val cd: Path.T -> Toplevel.transition -> Toplevel.transition
   val pwd: Toplevel.transition -> Toplevel.transition
   val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
   val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition

 val back =
   Toplevel.actual_proof ProofHistory.back o
   Toplevel.skip_proof (History.apply I);
 
 
-(* use ML text *)
-
-fun use path = Toplevel.keep (fn state =>
-  Context.setmp_thread_data (try Toplevel.generic_theory_of state) (ThyInfo.load_file false) path);
-
-(*passes changes of theory context*)
-fun use_mltext_theory (txt, pos) = Toplevel.theory' (fn int =>
-  Context.theory_map (ML_Context.exec (fn () => ML_Context.eval int pos txt)));
-
-(*ignore result theory context*)
-fun use_mltext verbose (txt, pos) = Toplevel.keep' (fn int => fn state =>
-  (ML_Context.eval_in (try Toplevel.generic_theory_of state) (verbose andalso int) pos txt));
-
-val use_commit = Toplevel.imperative Secure.commit;
+(* diagnostic ML evaluation *)
+
+fun ml_diag verbose (txt, pos) = Toplevel.keep (fn state =>
+  (ML_Context.eval_in (try Toplevel.generic_theory_of state) verbose pos txt));
 
 
 (* nested commands *)
 
 fun nested_command props (str, pos) =