src/HOL/Codatatype/Examples/Misc_Data.thy
changeset 50451 37cae324d73e
parent 50234 c28dd8326f9a
child 50471 fa8302c8dea1
     1.1 --- a/src/HOL/Codatatype/Examples/Misc_Data.thy	Tue Sep 18 11:06:25 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Examples/Misc_Data.thy	Tue Sep 18 11:41:04 2012 +0200
     1.3 @@ -145,8 +145,8 @@
     1.4   and s8 = S8 nat
     1.5  *)
     1.6  
     1.7 -data ('a, 'b) bar = BAR "'b \<Rightarrow> 'a"
     1.8 -data ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \<Rightarrow> 'c + 'a"
     1.9 +data ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
    1.10 +data ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
    1.11  
    1.12  data 'a dead_foo = A
    1.13  data ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"