# HG changeset patch
# User wenzelm
# Date 1459886864 -7200
# Node ID 20b0cb2f0b87f5a2af360b678035632dc37dfe8f
# Parent  76e7d9169b54ac64c2fd37a829c3aff66eaf79c5
proper file extension;

diff -r 76e7d9169b54 -r 20b0cb2f0b87 src/Pure/ML/ml_root.scala
--- a/src/Pure/ML/ml_root.scala	Tue Apr 05 21:51:14 2016 +0200
+++ b/src/Pure/ML/ml_root.scala	Tue Apr 05 22:07:44 2016 +0200
@@ -23,7 +23,7 @@
       (USE, Some((Keyword.THY_LOAD, Nil)), None) +
       (USE_DEBUG, Some((Keyword.THY_LOAD, Nil)), None) +
       (USE_NO_DEBUG, Some((Keyword.THY_LOAD, Nil)), None) +
-      (USE_THY, Some((Keyword.THY_LOAD, Nil)), None)
+      (USE_THY, Some((Keyword.THY_LOAD, List("thy"))), None)
 
   private object Parser extends Parse.Parser
   {
diff -r 76e7d9169b54 -r 20b0cb2f0b87 src/Pure/ML_Root.thy
--- a/src/Pure/ML_Root.thy	Tue Apr 05 21:51:14 2016 +0200
+++ b/src/Pure/ML_Root.thy	Tue Apr 05 22:07:44 2016 +0200
@@ -7,7 +7,7 @@
 theory ML_Root
 imports Pure
 keywords "use" "use_debug" "use_no_debug" :: thy_load
-  and "use_thy" :: thy_load
+  and "use_thy" :: thy_load ("thy")
 begin
 
 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>