src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy

--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Tue Sep 07 10:05:19 2010 +0200
@@ -31,7 +31,7 @@
 
 lemma [code_pred_inline]:
   "max = max_nat"
-by (simp add: expand_fun_eq max_def max_nat_def)
+by (simp add: ext_iff max_def max_nat_def)
 
 definition
   "max_of_my_Suc x = max x (Suc x)"