src/HOL/BNF/Examples/TreeFsetI.thy
changeset 51804 be6e703908f4
parent 51410 f0865a641e76
child 53013 3fbcfa911863
--- a/src/HOL/BNF/Examples/TreeFsetI.thy	Mon Apr 29 06:13:36 2013 +0200
+++ b/src/HOL/BNF/Examples/TreeFsetI.thy	Mon Apr 29 09:10:49 2013 +0200
@@ -14,7 +14,7 @@
 
 hide_fact (open) Quotient_Product.prod_rel_def
 
-codata 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
+codatatype 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
 
 definition pair_fun (infixr "\<odot>" 50) where
   "f \<odot> g \<equiv> \<lambda>x. (f x, g x)"