# HG changeset patch
# User wenzelm
# Date 1406202480 -7200
# Node ID 858bee39acdec53e1749cd645a615fc4cfa28986
# Parent  dc59f147b27d2ed2c8a9ebef53dbb66017f82761
make SML/NJ happy;

diff -r dc59f147b27d -r 858bee39acde 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);