# HG changeset patch
# User wenzelm
# Date 1279643599 -7200
# Node ID 173974e07dea2411d977504506539766785fb845
# Parent  1ad8205078d429c3841850a392ae72aa3422277d
Topelevel.run_command: interactive mode for initial 'theory' ensures that Thy_Info.begin_theory loads parent theories;

diff -r 1ad8205078d4 -r 173974e07dea src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Jul 20 18:19:50 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 20 18:33:19 2010 +0200
@@ -630,7 +630,7 @@
         SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
       | NONE => Exn.Result ()) of
     Exn.Result () =>
-      (case transition false tr st of
+      (case transition (is_some (init_of tr)) tr st of
         SOME (st', NONE) => (status tr Markup.finished; async_state tr st'; SOME st')
       | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
       | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)