# HG changeset patch
# User blanchet
# Date 1410181955 -7200
# Node ID 7f5d72a681a21bdae1b0029f9dd257f620acde38
# Parent  d91f7a80f41271991cb3956b40645f8e7e462421
test sorts

diff -r d91f7a80f412 -r 7f5d72a681a2 src/HOL/BNF_Examples/Misc_Codatatype.thy
--- 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 =
diff -r d91f7a80f412 -r 7f5d72a681a2 src/HOL/BNF_Examples/Misc_Datatype.thy
--- 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"