# HG changeset patch
# User kuncar
# Date 1332768808 -7200
# Node ID 9890d4f0c1db02fde9d259901c0c19827c7fe790
# Parent  529d2a949bd49ee56c14c86596d50d1f3a51d0f7# Parent  b5a5662528fb9f5b401a5c56e308ff5ee9771fad
merged

diff -r b5a5662528fb -r 9890d4f0c1db src/HOL/Quotient_Examples/Lift_Fun.thy
--- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Sat Mar 24 20:24:16 2012 +0100
+++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Mon Mar 26 15:33:28 2012 +0200
@@ -85,7 +85,10 @@
   unfolding endofun_rel_def map_endofun_def map_fun_def o_def map_endofun'_def endofun_rel'_def id_def 
     by (metis (mono_tags) Quotient_endofun rep_abs_rsp)
 next
-  show "\<And>r s. endofun_rel R r s =
+  have abs_to_eq: "\<And> x y. abs_endofun x = abs_endofun y \<Longrightarrow> x = y" 
+  by (drule arg_cong[where f=rep_endofun]) (simp add: Quotient_rep_abs[OF Quotient_endofun])
+  fix r s
+  show "endofun_rel R r s =
           (endofun_rel R r r \<and>
            endofun_rel R s s \<and> map_endofun Abs Rep r = map_endofun Abs Rep s)"
     apply(auto simp add: endofun_rel_def endofun_rel'_def map_endofun_def map_endofun'_def)
@@ -95,8 +98,7 @@
     apply metis
     using fun_quotient[OF a a, THEN Quotient_rel]
     apply metis
-    using fun_quotient[OF a a, THEN Quotient_rel]
-    by (smt Quotient_endofun rep_abs_rsp)
+    by (auto intro: fun_quotient[OF a a, THEN Quotient_rel, THEN iffD1] simp add: abs_to_eq)
 qed
 
 declare [[map endofun = (endofun_rel, endofun_quotient)]]