# HG changeset patch
# User wenzelm
# Date 1206814451 -3600
# Node ID e83dc4bb9ab4541fcd33bf12bb89fa7dcd0f3823
# Parent  b497e3187ec72a6a23c24c38c882da85006544f8
removed obsolete use_XXX;
added ml_diag;

diff -r b497e3187ec7 -r e83dc4bb9ab4 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Mar 29 19:14:10 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Mar 29 19:14:11 2008 +0100
@@ -62,10 +62,7 @@
   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
@@ -382,20 +379,10 @@
   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);
+(* diagnostic ML evaluation *)
 
-(*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;
+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 *)