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