src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 39650 2a35950ec495
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Sep 13 11:13:15 2010 +0200
@@ -12,7 +12,7 @@
 declare le_bool_def_raw[code_pred_inline]
 
 lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op &)"
-by (rule eq_reflection) (auto simp add: ext_iff min_def le_bool_def)
+by (rule eq_reflection) (auto simp add: fun_eq_iff min_def le_bool_def)
 
 setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}