src/Pure/ROOT.ML

--- a/src/Pure/ROOT.ML	Mon Aug 17 21:22:55 2015 +0200
+++ b/src/Pure/ROOT.ML	Mon Aug 17 21:32:41 2015 +0200
@@ -41,24 +41,11 @@
 val use_text = Secure.use_text;
 val use_file = Secure.use_file;
 
-local
-  fun use_ debug_option file =
-    let
-      val debug =
-        (case debug_option of
-          SOME debug => debug
-        | NONE => getenv "ISABELLE_ML_DEBUGGER" = "true");
-    in
-      Position.setmp_thread_data (Position.file_only file)
-        (fn () =>
-          Secure.use_file ML_Parse.global_context {verbose = true, debug = debug} file
-            handle ERROR msg => (writeln msg; error "ML error")) ()
-    end;
-in
-  val use = use_ NONE;
-  val use_debug = use_ (SOME true);
-  val use_no_debug = use_ (SOME false);
-end;
+fun use file =
+  Position.setmp_thread_data (Position.file_only file)
+    (fn () =>
+      Secure.use_file ML_Parse.global_context {verbose = true, debug = false} file
+        handle ERROR msg => (writeln msg; error "ML error")) ();
 
 val toplevel_pp = Secure.toplevel_pp;
 
@@ -257,21 +244,9 @@
 use "ML/ml_context.ML";
 use "ML/ml_antiquotation.ML";
 
-local
-  fun use_ debug file =
-    let
-      val flags: ML_Compiler.flags =
-        {SML = false, exchange = false, redirect = false, verbose = true,
-          debug = debug, writeln = writeln, warning = warning};
-    in
-      ML_Context.eval_file flags (Path.explode file)
-        handle ERROR msg => (writeln msg; error "ML error")
-    end;
-in
-  val use = use_ NONE;
-  val use_debug = use_ (SOME true);
-  val use_no_debug = use_ (SOME false);
-end;
+fun use s =
+  ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
+    handle ERROR msg => (writeln msg; error "ML error");