src/Pure/Thy/thy_load.ML

--- 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