diff -r bf31fd0231ba -r ebfc41a47641 src/HOL/Corec_Examples/Tests/Small_Concrete.thy
--- a/src/HOL/Corec_Examples/Tests/Small_Concrete.thy	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Corec_Examples/Tests/Small_Concrete.thy	Mon Mar 28 12:05:47 2016 +0200
@@ -146,11 +146,16 @@
     LNil \<Rightarrow> LNil
   | LCons x r \<Rightarrow> LCons x (h3 r))"
 
-corec (friend) fold_map where
+corec fold_map where
   "fold_map f a s = (let v = f a (head s) in S v (fold_map f v (tail s)))"
 
+friend_of_corec fold_map where
+  "fold_map f a s = (let v = f a (head s) in S v (fold_map f v (tail s)))"
+   apply (rule fold_map.code)
+  sorry
 
-subsection \<open>Coinductie Natural Numbers\<close>
+
+subsection \<open>Coinductive Natural Numbers\<close>
 
 codatatype conat = CoZero | CoSuc conat