src/Pure/PIDE/resources.ML

--- a/src/Pure/PIDE/resources.ML	Mon Aug 11 22:59:38 2014 +0200
+++ b/src/Pure/PIDE/resources.ML	Tue Aug 12 00:08:32 2014 +0200
@@ -132,7 +132,7 @@
 fun excursion master_dir last_timing init elements =
   let
     fun prepare_span span =
-      Thy_Syntax.span_content span
+      Command_Span.content span
       |> Command.read init master_dir []
       |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
 
@@ -157,8 +157,8 @@
     val _ = Thy_Header.define_keywords header;
 
     val lexs = Keyword.get_lexicons ();
-    val toks = Thy_Syntax.parse_tokens lexs text_pos text;
-    val spans = Thy_Syntax.parse_spans toks;
+    val toks = Outer_Syntax.parse_tokens lexs text_pos text;
+    val spans = Outer_Syntax.parse_spans toks;
     val elements = Thy_Syntax.parse_elements spans;
 
     fun init () =