# HG changeset patch
# User wenzelm
# Date 880201603 -3600
# Node ID 835ea07170a6cba80d5e4533edd3e961baada9dd
# Parent  c64867c093fbcf812afa587625995da4597638a6
made SML/NJ happy;

diff -r c64867c093fb -r 835ea07170a6 src/Pure/seq.ML
--- a/src/Pure/seq.ML	Sat Nov 22 13:26:30 1997 +0100
+++ b/src/Pure/seq.ML	Sat Nov 22 13:26:43 1997 +0100
@@ -44,7 +44,7 @@
 
 
 (*the empty sequence*)
-val empty = make (fn () => None);
+val empty = Seq (fn () => None);
 
 (*prefix an element to the sequence -- use cons (x, xq) only if
   evaluation of xq need not be delayed, otherwise use