--- a/src/Pure/ML_Bootstrap.thy Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/ML_Bootstrap.thy Thu Apr 07 16:53:43 2016 +0200
@@ -6,31 +6,10 @@
theory ML_Bootstrap
imports Pure
-keywords "use" "use_debug" "use_no_debug" :: thy_load
begin
setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
SML_import \<open>structure Thread_Data = Thread_Data_Virtual\<close>
-
-ML \<open>
-local
-
-val _ =
- Outer_Syntax.command @{command_keyword use}
- "read and evaluate Isabelle/ML or SML file"
- (Resources.parse_files "use" --| @{keyword ";"} >> ML_File.use NONE);
-
-val _ =
- Outer_Syntax.command @{command_keyword use_debug}
- "read and evaluate Isabelle/ML or SML file (with debugger information)"
- (Resources.parse_files "use_debug" --| @{keyword ";"} >> ML_File.use (SOME true));
-
-val _ =
- Outer_Syntax.command @{command_keyword use_no_debug}
- "read and evaluate Isabelle/ML or SML file (no debugger information)"
- (Resources.parse_files "use_no_debug" --| @{keyword ";"} >> ML_File.use (SOME false));
-
-in end
-\<close>
+setup \<open>Config.put_global ML_Env.SML_environment true\<close>
end