--- a/src/HOL/BNF_Examples/Misc_Codatatype.thy Mon Sep 08 15:11:37 2014 +0200
+++ b/src/HOL/BNF_Examples/Misc_Codatatype.thy Mon Sep 08 15:12:35 2014 +0200
@@ -23,7 +23,7 @@
codatatype 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist")
-codatatype ('b, 'c, 'd, 'e) some_passive =
+codatatype ('b, 'c :: ord, 'd, 'e) some_passive =
SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
codatatype lambda =
--- a/src/HOL/BNF_Examples/Misc_Datatype.thy Mon Sep 08 15:11:37 2014 +0200
+++ b/src/HOL/BNF_Examples/Misc_Datatype.thy Mon Sep 08 15:12:35 2014 +0200
@@ -21,7 +21,7 @@
datatype_new (discs_sels) 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist")
-datatype_new (discs_sels) ('b, 'c, 'd, 'e) some_passive =
+datatype_new (discs_sels) ('b, 'c :: ord, 'd, 'e) some_passive =
SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
datatype_new (discs_sels) hfset = HFset "hfset fset"