--- a/QuotMain.thy	Sun Sep 20 05:48:49 2009 +0100
+++ b/QuotMain.thy	Mon Sep 21 10:53:01 2009 +0200
@@ -29,8 +29,9 @@
 qed
 
 theorem thm10:
-  shows "ABS (REP a) = a"
-unfolding ABS_def REP_def
+  shows "ABS (REP a) \<equiv> a"
+  apply  (rule eq_reflection)
+  unfolding ABS_def REP_def
 proof -
   from rep_prop
   obtain x where eq: "Rep a = R x" by auto
@@ -761,7 +762,7 @@
      (UNION EMPTY s = s) &
      ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))"
   apply (simp add: yyy)
-  apply (rule QUOT_TYPE_I_fset.thm10)
+  apply (simp add: QUOT_TYPE_I_fset.thm10)
   done
 
 ML {*
@@ -935,20 +936,16 @@
   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
-    (* Why doesn't this work? *)
-  val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10 QUOT_TYPE_I_fset.REPS_same} cgoal2)
+  val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2)
 *}
-thm QUOT_TYPE_I_fset.thm10
-thm QUOT_TYPE_I_fset.REPS_same
 
-(* keep it commented out, until we get a proving mechanism *)
-(*prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *}*)
-lemma zzz : 
-  "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> 
+(* It is the same, but we need a name for it. *)
+prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} sorry
+lemma zzz :
+  "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx>
     REP_fset (INSERT a (ABS_fset xs))) =  (a # a # xs \<approx> a # xs)"
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-(*  apply (simp only: QUOT_TYPE_I_fset.thm10)*)
   apply (rule QUOT_TYPE_I_fset.R_trans2)
   apply (tactic {* foo_tac' 1 *})
   apply (tactic {* foo_tac' 1 *})
@@ -960,6 +957,13 @@
   apply (tactic {* foo_tac' 1 *})
   done
 
+lemma zzz' :
+  "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))"
+  using list_eq.intros(4) by (simp only: zzz)
+
+thm QUOT_TYPE_I_fset.REPS_same
+ML {* MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *}
+
 thm list_eq.intros(5)
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)}))