diff -r c7b06cdf108a -r d9be905d6283 src/HOL/BNF_Examples/Stream.thy
--- a/src/HOL/BNF_Examples/Stream.thy	Tue Jun 10 19:51:00 2014 +0200
+++ b/src/HOL/BNF_Examples/Stream.thy	Tue Jun 10 21:15:57 2014 +0200
@@ -12,8 +12,11 @@
 imports "~~/src/HOL/Library/Nat_Bijection"
 begin
 
-codatatype (sset: 'a) stream (map: smap rel: stream_all2) =
+codatatype (sset: 'a) stream =
   SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
+for
+  map: smap
+  rel: stream_all2
 
 (*for code generation only*)
 definition smember :: "'a \<Rightarrow> 'a stream \<Rightarrow> bool" where