src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy

--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Mon Sep 13 11:13:15 2010 +0200
@@ -31,7 +31,7 @@
 
 lemma [code_pred_inline]:
   "max = max_nat"
-by (simp add: ext_iff max_def max_nat_def)
+by (simp add: fun_eq_iff max_def max_nat_def)
 
 definition
   "max_of_my_Suc x = max x (Suc x)"