
diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Recdef.thy
--- a/src/HOL/Recdef.thy	Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Recdef.thy	Tue Sep 07 10:05:19 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: expand_fun_eq cut_def)
+by (simp add: ext_iff cut_def)
 
 lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
 by (simp add: cut_def)




