src/Pure/PIDE/document.ML
changeset 57905 c0c5652e796e
parent 57874 9c361f94b323
child 57918 f5d73caba4e5
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Aug 11 22:59:38 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Aug 12 00:08:32 2014 +0200
     1.3 @@ -318,7 +318,7 @@
     1.4        val span =
     1.5          Lazy.lazy (fn () =>
     1.6            Position.setmp_thread_data (Position.id_only id)
     1.7 -            (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id) text) ());
     1.8 +            (fn () => Outer_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id) text) ());
     1.9        val _ =
    1.10          Position.setmp_thread_data (Position.id_only id)
    1.11            (fn () => Output.status (Markup.markup_only Markup.accepted)) ();