src/Pure/Isar/isar_syn.ML

--- a/src/Pure/Isar/isar_syn.ML	Wed Jul 21 15:44:36 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jul 21 16:14:16 2010 +0200
@@ -314,7 +314,7 @@
 val _ =
   Outer_Syntax.command "use" "ML text from file" (Keyword.tag_ml Keyword.thy_decl)
     (Parse.path >>
-      (fn path => Toplevel.generic_theory (Thy_Info.exec_file false path #> propagate_env)));
+      (fn path => Toplevel.generic_theory (Thy_Info.exec_file path #> propagate_env)));
 
 val _ =
   Outer_Syntax.command "ML" "ML text within theory or local theory"