
diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/UNITY/Lift_prog.thy
--- a/src/HOL/UNITY/Lift_prog.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/UNITY/Lift_prog.thy	Mon Sep 13 11:13:15 2010 +0200
@@ -337,10 +337,10 @@
 
 (*Lets us prove one version of a theorem and store others*)
 lemma o_equiv_assoc: "f o g = h ==> f' o f o g = f' o h"
-by (simp add: ext_iff o_def)
+by (simp add: fun_eq_iff o_def)
 
 lemma o_equiv_apply: "f o g = h ==> \<forall>x. f(g x) = h x"
-by (simp add: ext_iff o_def)
+by (simp add: fun_eq_iff o_def)
 
 lemma fst_o_lift_map: "sub i o fst o lift_map i = fst"
 apply (rule ext)




