load_thy: try_ml_file unconditionally;
authorwenzelm
Wed Aug 08 23:07:47 2007 +0200 (2007-08-08)
changeset 24188d5960310c4d5
parent 24187 8bdf5ca5871f
child 24189 1fa9852643a3
load_thy: try_ml_file unconditionally;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed Aug 08 23:07:46 2007 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Wed Aug 08 23:07:47 2007 +0200
     1.3 @@ -278,10 +278,10 @@
     1.4      val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
     1.5    in () end;
     1.6  
     1.7 -fun load_thy dir name pos text ml time =
     1.8 +fun load_thy dir name pos text time =
     1.9   (run_thy dir name pos text time;
    1.10    CRITICAL (fn () => ML_Context.set_context (SOME (Context.Theory (ThyInfo.get_theory name))));
    1.11 -  if ml then try_ml_file dir name time else ());
    1.12 +  try_ml_file dir name time);
    1.13  
    1.14  in
    1.15