src/Pure/ML_Root.thy
changeset 62883 b04e9fe29223
parent 62881 20b0cb2f0b87
--- 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>