# HG changeset patch
# User kuncar
# Date 1332768774 -7200
# Node ID 529d2a949bd49ee56c14c86596d50d1f3a51d0f7
# Parent  35807a5d8dc25776809314154a8099cb588201a5
tuned proof - no smt call

diff -r 35807a5d8dc2 -r 529d2a949bd4 src/HOL/Quotient_Examples/Lift_Fun.thy
--- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Sat Mar 24 16:27:04 2012 +0100
+++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Mon Mar 26 15:32:54 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)]]