src/Pure/Isar/toplevel.ML

   Thread.fork
     (((fn () => body () handle Exn.Interrupt => ())
         |> Runtime.debugging
         |> Runtime.toplevel_error
           (fn exn => priority ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
-      SimpleThread.attributes interrupts);
+      Simple_Thread.attributes interrupts);
 
 
 (* node transactions -- maintaining stable checkpoints *)
 
 exception FAILURE of state * exn;

   in (st', st') end;
 
 fun run_command thy_name tr st =
   (case
       (case init_of tr of
-        SOME name => Exn.capture (fn () => ThyLoad.check_name thy_name name) ()
+        SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
       | NONE => Exn.Result ()) of
     Exn.Result () =>
       (case transition true tr st of
         SOME (st', NONE) => (status tr Markup.finished; SOME st')
       | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn