make SML/NJ happy;
authorwenzelm
Thu, 24 Jul 2014 13:48:00 +0200
changeset 57643 858bee39acde
parent 57641 dc59f147b27d
child 57644 6ca1646b6f14
make SML/NJ happy;
src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Jul 24 11:54:15 2014 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Jul 24 13:48:00 2014 +0200
@@ -72,7 +72,7 @@
   visible_last = try List.last command_ids,
   overlays = Inttab.make_list overlays};
 
-val no_header = ("", Thy_Header.make ("", Position.none) [] [], []);
+val no_header: node_header = ("", Thy_Header.make ("", Position.none) [] [], []);
 val no_perspective = make_perspective (false, [], []);
 
 val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);