diff -r f7c00119e6e7 -r ca53150406c9 src/HOL/Library/Stream.thy
--- a/src/HOL/Library/Stream.thy	Sat Nov 14 18:37:49 2015 +0100
+++ b/src/HOL/Library/Stream.thy	Sun Nov 15 12:39:51 2015 +0100
@@ -68,12 +68,18 @@
 
 subsection \<open>set of streams with elements in some fixed set\<close>
 
+context
+  notes [[inductive_defs]]
+begin
+
 coinductive_set
   streams :: "'a set \<Rightarrow> 'a stream set"
   for A :: "'a set"
 where
   Stream[intro!, simp, no_atp]: "\<lbrakk>a \<in> A; s \<in> streams A\<rbrakk> \<Longrightarrow> a ## s \<in> streams A"
 
+end
+
 lemma in_streams: "stl s \<in> streams S \<Longrightarrow> shd s \<in> S \<Longrightarrow> s \<in> streams S"
   by (cases s) auto