src/Pure/PIDE/document.ML
changeset 43761 e72ba84ae58f
parent 43722 9b5dadb0c28d
child 44113 0baa8bbd355a
--- a/src/Pure/PIDE/document.ML	Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Jul 11 22:55:47 2011 +0200
@@ -252,8 +252,8 @@
             val path = Path.explode thy_name;
             val _ = Thy_Header.consistent_name (Path.implode (Path.base path)) name;
           in Toplevel.modify_master (SOME (Path.dir path)) raw_tr end) ()
-      | NONE => Exn.Result raw_tr) of
-    Exn.Result tr =>
+      | NONE => Exn.Res raw_tr) of
+    Exn.Res tr =>
       let
         val is_init = is_some (Toplevel.init_of tr);
         val is_proof = Keyword.is_proof (Toplevel.name_of tr);