diff -r 3c4161728aa8 -r b04e9fe29223 src/Pure/ML_Root.thy --- 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 \Context.theory_map ML_Env.init_bootstrap\ @@ -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 \