src/Pure/PIDE/isar_document.ML
changeset 43767 e0219ef7f84c
parent 43748 c70bd78ec83c
child 44156 6aa25b80e1a5
     1.1 --- a/src/Pure/PIDE/isar_document.ML	Tue Jul 12 16:00:05 2011 +0900
     1.2 +++ b/src/Pure/PIDE/isar_document.ML	Tue Jul 12 10:44:30 2011 +0200
     1.3 @@ -18,10 +18,10 @@
     1.4          val old_id = Document.parse_id old_id_string;
     1.5          val new_id = Document.parse_id new_id_string;
     1.6          val edits = YXML.parse_body edits_yxml |>
     1.7 -          let open XML_Data.Decode
     1.8 +          let open XML.Decode
     1.9            in list (pair string (option (list (pair (option int) (option int))))) end;
    1.10          val headers = YXML.parse_body headers_yxml |>
    1.11 -          let open XML_Data.Decode
    1.12 +          let open XML.Decode
    1.13            in list (pair string (triple string (list string) (list string))) end;
    1.14  
    1.15        val await_cancellation = Document.cancel_execution state;