# HG changeset patch
# User krauss
# Date 1298389638 -3600
# Node ID c7be23634728c7a74bcd7085c62c2a782b0b678c
# Parent  7a55699805dc4c3d5398cef0b42334cd52eb4fff
dropped obsolete FIXMEs

diff -r 7a55699805dc -r c7be23634728 src/HOL/ex/Fundefs.thy
--- a/src/HOL/ex/Fundefs.thy	Mon Feb 21 23:54:53 2011 +0100
+++ b/src/HOL/ex/Fundefs.thy	Tue Feb 22 16:47:18 2011 +0100
@@ -280,14 +280,12 @@
 
 
 (* There were some problems with fresh names\<dots> *)
-(* FIXME: tailrec? *)
 function  k :: "nat \<Rightarrow> nat"
 where
   "k x = (let a = x; b = x in k x)"
   by pat_completeness auto
 
 
-(* FIXME: tailrec? *)
 function f2 :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 where
   "f2 p = (let (x,y) = p in f2 (y,x))"