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