src/HOL/Datatype_Examples/Misc_Datatype.thy

 (*
   ('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2
   ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2
 *)
 
-datatype (discs_sels) 'a I1 = I11 'a "'a I1" | I12 'a "'a I2"
-and 'a I2 = I21 | I22 "'a I1" "'a I2"
-
-datatype (discs_sels) 'a tree = TEmpty | TNode 'a "'a forest"
-and 'a forest = FNil | FCons "'a tree" "'a forest"
+locale loc =
+  fixes c :: 'a and d :: 'a
+  assumes "c \<noteq> d"
+begin
+
+datatype (discs_sels) 'b I1 = I11 'b "'b I1" | I12 'b "'b I2"
+and 'b I2 = I21 | I22 "'b I1" "'b I2"
+
+datatype (discs_sels) 'b tree = TEmpty | TNode 'b "'b forest"
+and 'b forest = FNil | FCons "'b tree" "'b forest"
+
+end
 
 datatype (discs_sels) 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
 and 'a branch = Branch 'a "'a tree'"
 
 datatype (discs_sels) 'a bin_rose_tree = BRTree 'a "'a bin_rose_tree mylist" "'a bin_rose_tree mylist"

 
 instance par_lambda :: (countable) countable
   by countable_datatype
 *)
 
-instance I1 and I2 :: (countable) countable
-  by countable_datatype
-
-instance tree and forest :: (countable) countable
-  by countable_datatype
-
 instance tree' and branch :: (countable) countable
   by countable_datatype
 
 instance bin_rose_tree :: (countable) countable
   by countable_datatype

 datatype_compat simple
 datatype_compat simple'
 datatype_compat simple''
 datatype_compat mylist
 datatype_compat some_passive
-datatype_compat I1 I2
-datatype_compat tree forest
 datatype_compat tree' branch
 datatype_compat bin_rose_tree
 datatype_compat exp trm factor
 datatype_compat ftree
 datatype_compat nofail1