src/HOL/Recdef.thy

--- a/src/HOL/Recdef.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Recdef.thy	Mon Sep 13 11:13:15 2010 +0200
@@ -45,7 +45,7 @@
 text{*cut*}
 
 lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
-by (simp add: ext_iff cut_def)
+by (simp add: fun_eq_iff cut_def)
 
 lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
 by (simp add: cut_def)