# HG changeset patch
# User blanchet
# Date 1410185661 -7200
# Node ID ad45b22a0b3935f1c55dca5904d5ea0a07ba4399
# Parent  61e4c96bf2b6c4d95faec59b1617c58edfc3f768
adapted examples to latest changes

diff -r 61e4c96bf2b6 -r ad45b22a0b39 src/HOL/BNF_Examples/Misc_Primcorec.thy
--- 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')
diff -r 61e4c96bf2b6 -r ad45b22a0b39 src/HOL/BNF_Examples/Misc_Primrec.thy
--- 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" |
diff -r 61e4c96bf2b6 -r ad45b22a0b39 src/HOL/ex/Refute_Examples.thy
--- 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]