# HG changeset patch
# User blanchet
# Date 1346854059 -7200
# Node ID e075733fa8c2f895194bf2a70f07a6ada39e6db1
# Parent  c6ccaf6df93c4b77711fe3172ea9bab187ca62a9
adapted example

diff -r c6ccaf6df93c -r e075733fa8c2 src/HOL/Codatatype/Examples/Misc_Data.thy
--- a/src/HOL/Codatatype/Examples/Misc_Data.thy	Wed Sep 05 16:00:53 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Misc_Data.thy	Wed Sep 05 16:07:39 2012 +0200
@@ -61,8 +61,7 @@
   IH1 'b 'a | IH2 'c
 *)
 
-(* FIXME data 'b nofail1 = NF11 "'a \<times> 'b" | NF12 'b *)
-data_raw nofail1: 'a = "'a \<times> 'b + 'b"
+data 'b nofail1 = NF11 "'b nofail1 \<times> 'b" | NF12 'b
 data 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list"
 data 'b nofail3 = NF3 "'b \<times> ('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset"
 data 'b nofail4 = NF4 "('b nofail3 \<times> ('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset) list"