--- a/src/HOL/UNITY/Rename.thy Sun Jan 30 20:48:50 2005 +0100
+++ b/src/HOL/UNITY/Rename.thy Tue Feb 01 18:01:57 2005 +0100
@@ -110,8 +110,8 @@
lemma bij_extend: "bij h ==> bij (extend (%(x,u::'c). h x))"
apply (rule bijI)
apply (blast intro: Extend.inj_extend)
-apply (rule_tac f = "extend (% (x,u) . inv h x) " in surjI)
-apply (subst inv_inv_eq [of h, symmetric], assumption)
+apply (rule_tac f = "extend (% (x,u) . inv h x) " in surjI)
+apply (simplesubst inv_inv_eq [of h, symmetric], assumption)
apply (subst extend_inv, simp add: bij_imp_bij_inv)
apply (simp add: inv_inv_eq)
apply (rule Extend.extend_inverse)