Topelevel.run_command: interactive mode for initial 'theory' ensures that Thy_Info.begin_theory loads parent theories;
authorwenzelm
Tue Jul 20 18:33:19 2010 +0200 (2010-07-20 ago)
changeset 37856173974e07dea
parent 37855 1ad8205078d4
child 37857 4e4b8c0dc766
Topelevel.run_command: interactive mode for initial 'theory' ensures that Thy_Info.begin_theory loads parent theories;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Jul 20 18:19:50 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Jul 20 18:33:19 2010 +0200
     1.3 @@ -630,7 +630,7 @@
     1.4          SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
     1.5        | NONE => Exn.Result ()) of
     1.6      Exn.Result () =>
     1.7 -      (case transition false tr st of
     1.8 +      (case transition (is_some (init_of tr)) tr st of
     1.9          SOME (st', NONE) => (status tr Markup.finished; async_state tr st'; SOME st')
    1.10        | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
    1.11        | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)