--- a/src/HOL/BNF_Examples/Misc_Primcorec.thy Mon Sep 08 16:09:10 2014 +0200
+++ b/src/HOL/BNF_Examples/Misc_Primcorec.thy Mon Sep 08 16:14:21 2014 +0200
@@ -30,7 +30,7 @@
else if ys = MyNil then xs
else MyCons (myhd xs) (myapp (mytl xs) ys))"
-primcorec shuffle_sp :: "('a, 'b, 'c, 'd) some_passive \<Rightarrow> ('d, 'a, 'b, 'c) some_passive" where
+primcorec shuffle_sp :: "('a \<Colon> ord, 'b \<Colon> ord, 'c, 'd) some_passive \<Rightarrow> ('d, 'a, 'b, 'c) some_passive" where
"shuffle_sp sp =
(case sp of
SP1 sp' \<Rightarrow> SP1 (shuffle_sp sp')
--- a/src/HOL/BNF_Examples/Misc_Primrec.thy Mon Sep 08 16:09:10 2014 +0200
+++ b/src/HOL/BNF_Examples/Misc_Primrec.thy Mon Sep 08 16:14:21 2014 +0200
@@ -35,7 +35,7 @@
"myrev MyNil = MyNil" |
"myrev (MyCons x xs) = myapp (myrev xs) (MyCons x MyNil)"
-primrec shuffle_sp :: "('a, 'b, 'c, 'd) some_passive \<Rightarrow> ('d, 'a, 'b, 'c) some_passive" where
+primrec shuffle_sp :: "('a \<Colon> ord, 'b \<Colon> ord, 'c, 'd) some_passive \<Rightarrow> ('d, 'a, 'b, 'c) some_passive" where
"shuffle_sp (SP1 sp) = SP1 (shuffle_sp sp)" |
"shuffle_sp (SP2 a) = SP3 a" |
"shuffle_sp (SP3 b) = SP4 b" |
--- a/src/HOL/ex/Refute_Examples.thy Mon Sep 08 16:09:10 2014 +0200
+++ b/src/HOL/ex/Refute_Examples.thy Mon Sep 08 16:14:21 2014 +0200
@@ -1065,8 +1065,8 @@
datatype_new Trie = TR "Trie list"
datatype_compat Trie
-abbreviation "rec_Trie_1 \<equiv> compat_Trie.n2m_Trie_rec"
-abbreviation "rec_Trie_2 \<equiv> compat_Trie_list.n2m_Trie_list_rec"
+abbreviation "rec_Trie_1 \<equiv> compat_Trie.rec_n2m_Trie"
+abbreviation "rec_Trie_2 \<equiv> compat_Trie_list.rec_n2m_Trie_list"
lemma "P (x::Trie)"
refute [expect = potential]