# HG changeset patch
# User wenzelm
# Date 1372931745 -7200
# Node ID ecc0e00077925d937cd824d520f7df3993beec29
# Parent  9a2cd366a322013747d91bbffdb9224a08bcf3f2
made SML/NJ happy;

diff -r 9a2cd366a322 -r ecc0e0007792 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Jul 04 09:13:49 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Jul 04 11:55:45 2013 +0200
@@ -65,7 +65,8 @@
 
 type exec = ((Toplevel.state * {malformed: bool}) * Command.print list) Command.memo;
   (*eval/print process*)
-val no_exec = Command.memo_value ((Toplevel.toplevel, {malformed = false}), []);
+val no_exec =
+  Command.memo_value ((Toplevel.toplevel, {malformed = false}), []: Command.print list);
 
 abstype node = Node of
  {header: node_header,  (*master directory, theory header, errors*)