--- a/src/Pure/ML_Root.thy Tue Apr 05 22:31:28 2016 +0200
+++ b/src/Pure/ML_Root.thy Wed Apr 06 11:37:37 2016 +0200
@@ -7,7 +7,6 @@
theory ML_Root
imports Pure
keywords "use" "use_debug" "use_no_debug" :: thy_load
- and "use_thy" :: thy_load ("thy")
begin
setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
@@ -30,11 +29,6 @@
"read and evaluate Isabelle/ML or SML file (no debugger information)"
(Resources.parse_files "use_no_debug" --| @{keyword ";"} >> ML_File.use (SOME false));
-val _ =
- Outer_Syntax.command @{command_keyword use_thy} "undefined dummy command"
- (Parse.path -- @{keyword ";"} >> (fn _ =>
- Toplevel.keep (fn _ => error "Undefined command 'use_thy'")));
-
in end
\<close>