src/Pure/Thy/thy_load.ML

--- a/src/Pure/Thy/thy_load.ML	Sun Mar 04 11:03:10 2012 +0100
+++ b/src/Pure/Thy/thy_load.ML	Sun Mar 04 16:02:14 2012 +0100
@@ -176,11 +176,10 @@
       begin_theory dir name imports uses parents
       |> Present.begin_theory update_time dir uses;
 
-    val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text));
-    val spans = Source.exhaust (Thy_Syntax.span_source toks);
+    val toks = Thy_Syntax.parse_tokens lexs pos text;
+    val spans = Thy_Syntax.parse_spans toks;
     val elements =
-      Source.exhaust (Thy_Syntax.element_source (Source.of_list spans))
-      |> maps (Outer_Syntax.read_element outer_syntax init);
+      maps (Outer_Syntax.read_element outer_syntax init) (Thy_Syntax.parse_elements spans);
 
     val _ = Present.theory_source name
       (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);