1.1 --- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Mon Mar 26 15:32:54 2012 +0200
     1.3 @@ -85,7 +85,10 @@
     1.4    unfolding endofun_rel_def map_endofun_def map_fun_def o_def map_endofun'_def endofun_rel'_def id_def 
     1.5      by (metis (mono_tags) Quotient_endofun rep_abs_rsp)
     1.6  next
     1.7 -  show "\<And>r s. endofun_rel R r s =
     1.8 +  have abs_to_eq: "\<And> x y. abs_endofun x = abs_endofun y \<Longrightarrow> x = y" 
     1.9 +  by (drule arg_cong[where f=rep_endofun]) (simp add: Quotient_rep_abs[OF Quotient_endofun])
    1.10 +  fix r s
    1.11 +  show "endofun_rel R r s =
    1.12            (endofun_rel R r r \<and>
    1.13             endofun_rel R s s \<and> map_endofun Abs Rep r = map_endofun Abs Rep s)"
    1.14      apply(auto simp add: endofun_rel_def endofun_rel'_def map_endofun_def map_endofun'_def)
    1.15 @@ -95,8 +98,7 @@
    1.16      apply metis
    1.17      using fun_quotient[OF a a, THEN Quotient_rel]
    1.18      apply metis
    1.19 -    using fun_quotient[OF a a, THEN Quotient_rel]
    1.20 -    by (smt Quotient_endofun rep_abs_rsp)
    1.21 +    by (auto intro: fun_quotient[OF a a, THEN Quotient_rel, THEN iffD1] simp add: abs_to_eq)
    1.22  qed
    1.23  
    1.24  declare [[map endofun = (endofun_rel, endofun_quotient)]]