# HG changeset patch
# User wenzelm
# Date 1186607267 -7200
# Node ID d5960310c4d539e5ca1812613233b569d8fb8bc1
# Parent  8bdf5ca5871f522293af205ac6d932a87eaf4346
load_thy: try_ml_file unconditionally;

diff -r 8bdf5ca5871f -r d5960310c4d5 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Aug 08 23:07:46 2007 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Aug 08 23:07:47 2007 +0200
@@ -278,10 +278,10 @@
     val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
   in () end;
 
-fun load_thy dir name pos text ml time =
+fun load_thy dir name pos text time =
  (run_thy dir name pos text time;
   CRITICAL (fn () => ML_Context.set_context (SOME (Context.Theory (ThyInfo.get_theory name))));
-  if ml then try_ml_file dir name time else ());
+  try_ml_file dir name time);
 
 in