--- a/src/HOLCF/ex/Dagstuhl.thy	Thu Jun 29 16:16:24 1995 +0200
+++ b/src/HOLCF/ex/Dagstuhl.thy	Thu Jun 29 16:28:40 1995 +0200
@@ -4,13 +4,14 @@
 Dagstuhl  =  Stream2 +
 
 consts
+	y  :: "'a"
        YS  :: "'a stream"
        YYS :: "'a stream"
 
-rules
+defs
 
-YS_def    "YS  = fix[LAM x. scons[y][x]]"
-YYS_def   "YYS = fix[LAM z. scons[y][scons[y][z]]]"
+YS_def    "YS  == fix`(LAM x. scons`y`x)"
+YYS_def   "YYS == fix`(LAM z. scons`y`(scons`y`z))"
   
 end