
diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/UNITY/Lift_prog.thy
--- a/src/HOL/UNITY/Lift_prog.thy	Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/UNITY/Lift_prog.thy	Tue Sep 07 10:05:19 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: expand_fun_eq o_def)
+by (simp add: ext_iff o_def)
 
 lemma o_equiv_apply: "f o g = h ==> \<forall>x. f(g x) = h x"
-by (simp add: expand_fun_eq o_def)
+by (simp add: ext_iff o_def)
 
 lemma fst_o_lift_map: "sub i o fst o lift_map i = fst"
 apply (rule ext)




