--- a/QuotMain.thy	Wed Sep 23 16:57:56 2009 +0200
+++ b/QuotMain.thy	Thu Sep 24 09:09:46 2009 +0200
@@ -950,15 +950,21 @@
 
 (* Has all the theorems about fset plugged in. These should be parameters to the tactic *)
 
+lemma trueprop_cong:
+  shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"
+  by auto
+
 ML {*
   fun foo_tac' ctxt =
     REPEAT_ALL_NEW (FIRST' [
+      rtac @{thm trueprop_cong},
       rtac @{thm list_eq_sym},
       rtac @{thm cons_preserves},
       rtac @{thm mem_respects},
       rtac @{thm QUOT_TYPE_I_fset.R_trans2},
       CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),
-      foo_tac
+      foo_tac,
+      CHANGED o (ObjectLogic.full_atomize_tac)
     ])
 *}
 
@@ -972,13 +978,7 @@
 (*notation ( output) "prop" ("#_" [1000] 1000) *)
 notation ( output) "Trueprop" ("#_" [1000] 1000)
 
-lemma tp:
-  shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"
-  by auto
-
 prove {* (Thm.term_of cgoal2) *}
-  apply (rule tp)
-  apply (tactic {* ObjectLogic.full_atomize_tac 1 *})
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (tactic {* foo_tac' @{context} 1 *})
   done
@@ -991,8 +991,6 @@
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
 prove {* Thm.term_of cgoal2 *}
-  apply (rule tp)
-  apply (tactic {* ObjectLogic.full_atomize_tac 1 *})
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (tactic {* foo_tac' @{context} 1 *})
   sorry
@@ -1005,8 +1003,6 @@
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
 prove {* Thm.term_of cgoal2 *}
-  apply (rule tp)
-  apply (tactic {* ObjectLogic.full_atomize_tac 1 *})
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (tactic {* foo_tac' @{context} 1 *})
   done
@@ -1022,16 +1018,12 @@
 
 (* It is the same, but we need a name for it. *)
 prove {* Thm.term_of cgoal3 *}
-  apply (rule tp)
-  apply (tactic {* ObjectLogic.full_atomize_tac 1 *})
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (tactic {* foo_tac' @{context} 1 *})
   done
 lemma zzz :
   "Trueprop (REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))
     \<equiv> Trueprop (a # a # xs \<approx> a # xs)"
-  apply (rule tp)
-  apply (tactic {* ObjectLogic.full_atomize_tac 1 *})
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (tactic {* foo_tac' @{context} 1 *})
   done
@@ -1072,9 +1064,6 @@
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
 prove {* Thm.term_of cgoal2 *}
-  apply (tactic {* ObjectLogic.full_atomize_tac 1 *})
-  apply (rule tp)
-  apply (tactic {* ObjectLogic.full_atomize_tac 1 *})
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (tactic {* foo_tac' @{context} 1 *})
   done