# HG changeset patch
# User blanchet
# Date 1459159547 -7200
# Node ID 8745b8079b97fa06478b18b0cc4c08871115469e
# Parent  b0bf94ccc59fd601638bd31a2255bc0668903ca0
FIXME

diff -r b0bf94ccc59f -r 8745b8079b97 src/HOL/Corec_Examples/Tests/Stream_Friends.thy
--- a/src/HOL/Corec_Examples/Tests/Stream_Friends.thy	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Corec_Examples/Tests/Stream_Friends.thy	Mon Mar 28 12:05:47 2016 +0200
@@ -45,9 +45,11 @@
   "sthe_default s _ None = s"
 | "sthe_default _ _ (Some t) = t"
 
+(* FIXME:
 friend_of_corec sthe_default where
   "sthe_default s n opt = SCons (shd (case opt of None \<Rightarrow> s | Some t \<Rightarrow> t)) (stl (case opt of None \<Rightarrow> s | Some t \<Rightarrow> t))"
   sorry
+*)
 
 corec funky0 :: "nat \<Rightarrow> nat stream" where
   "funky0 n = SCons 0 (sthe_default undefined n (map_option funky0 undefined))"
@@ -70,9 +72,11 @@
 corec phunky0 :: "nat \<Rightarrow> nat stream" where
   "phunky0 n = sthe_default undefined n undefined"
 
+(* FIXME:
 fun lthe_default :: "'a stream \<Rightarrow> 'a stream option \<Rightarrow> 'a stream" where
   "lthe_default s None = s"
 | "lthe_default _ (Some t) = t"
+*)
 
 friend_of_corec lthe_default where
   "lthe_default s opt = SCons (shd (case opt of None \<Rightarrow> s | Some t \<Rightarrow> t)) (stl (case opt of None \<Rightarrow> s | Some t \<Rightarrow> t))"