clarified Toplevel.element_result: scheduling policies happen here;
tuned;

--- a/src/Pure/Isar/toplevel.ML	Mon Feb 25 12:17:50 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Feb 25 12:52:27 2013 +0100
@@ -95,7 +95,7 @@
   val put_timing: Time.time -> transition -> transition
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
   val command: transition -> state -> state
-  val proof_result: bool -> transition * transition list -> state ->
+  val element_result: transition Thy_Syntax.element -> state ->
     (transition * state) list future * state
 end;
 
@@ -694,10 +694,6 @@
       if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)
   | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
 
-fun command_result tr st =
-  let val st' = command tr st
-  in ((tr, st'), st') end;
-
 
 (* scheduled proof result *)
 
@@ -708,13 +704,27 @@
   fun init _ = empty;
 );
 
-fun proof_result immediate (tr, proof_trs) st =
-  let val st' = command tr st in
-    if immediate orelse null proof_trs orelse not (can proof_of st') orelse
-      Proof.is_relevant (proof_of st')
+fun element_result (Thy_Syntax.Element (head_tr, opt_proof)) st =
+  let
+    val future_enabled = Goal.future_enabled ();
+
+    fun atom_result tr st =
+      let val st' = command tr st
+      in ((tr, st'), st') end;
+
+    val proof_trs =
+      (case opt_proof of
+        NONE => []
+      | SOME (a, b) => (maps Thy_Syntax.flat_element a @ [b]) |> filter_out is_ignored);
+
+    val st' = command head_tr st;
+  in
+    if not future_enabled orelse is_ignored head_tr orelse
+      Keyword.is_schematic_goal (name_of head_tr) orelse null proof_trs orelse
+      not (can proof_of st') orelse Proof.is_relevant (proof_of st')
     then
-      let val (results, st'') = fold_map command_result proof_trs st'
-      in (Future.value ((tr, st') :: results), st'') end
+      let val (results, st'') = fold_map atom_result proof_trs st'
+      in (Future.value (if is_ignored head_tr then results else (head_tr, st') :: results), st'') end
     else
       let
         val (body_trs, end_tr) = split_last proof_trs;
@@ -732,15 +742,15 @@
                 let val (result, result_state) =
                   (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
                     => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
-                  |> fold_map command_result body_trs ||> command end_tr;
+                  |> fold_map atom_result body_trs ||> command end_tr;
                 in (result, presentation_context_of result_state) end))
           #-> Result.put;
 
         val st'' = st'
-          |> command (tr |> set_print false |> reset_trans |> end_proof (K future_proof));
+          |> command (head_tr |> set_print false |> reset_trans |> end_proof (K future_proof));
         val result =
           Result.get (presentation_context_of st'')
-          |> Future.map (fn body => (tr, st') :: body @ [(end_tr, st'')]);
+          |> Future.map (fn body => (head_tr, st') :: body @ [(end_tr, st'')]);
 
       in (result, st'') end
   end;

--- a/src/Pure/Thy/thy_load.ML	Mon Feb 25 12:17:50 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Mon Feb 25 12:52:27 2013 +0100
@@ -216,8 +216,6 @@
 
 fun excursion last_timing init elements =
   let
-    val immediate = not (Goal.future_enabled ());
-
     fun prepare_span span =
       Thy_Syntax.span_content span
       |> Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ()))
@@ -226,28 +224,16 @@
 
     fun element_result span_elem (st, _) =
       let
-        val tr_elem = Thy_Syntax.map_element prepare_span span_elem;
-        val Thy_Syntax.Element (tr, opt_proof) = tr_elem;
-        val proof_trs =
-          (case opt_proof of
-            NONE => []
-          | SOME (a, b) => (maps Thy_Syntax.flat_element a @ [b]) |> filter_out Toplevel.is_ignored);
-
-        val elems =
-          if Toplevel.is_ignored tr then map (rpair []) proof_trs
-          else if Keyword.is_schematic_goal (Toplevel.name_of tr)
-          then map (rpair []) (tr :: proof_trs)
-          else [(tr, proof_trs)];
-
-        val (results, st') = fold_map (Toplevel.proof_result immediate) elems st;
-        val pos' = Toplevel.pos_of (Thy_Syntax.last_element tr_elem);
+        val elem = Thy_Syntax.map_element prepare_span span_elem;
+        val (results, st') = Toplevel.element_result elem st;
+        val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem);
       in (results, (st', pos')) end;
 
     val (results, (end_state, end_pos)) =
       fold_map element_result elements (Toplevel.toplevel, Position.none);
 
     val thy = Toplevel.end_theory end_pos end_state;
-  in (flat results, thy) end;
+  in (results, thy) end;
 
 fun load_thy last_timing update_time master_dir header text_pos text parents =
   let