--- a/QuotMain.thy	Tue Sep 29 17:46:18 2009 +0200
+++ b/QuotMain.thy	Tue Sep 29 22:35:48 2009 +0200
@@ -975,6 +975,9 @@
   shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"
   by auto
 
+ML {*
+  Cong_Tac.cong_tac
+*}
 
 thm QUOT_TYPE_I_fset.R_trans2
 ML {*
@@ -987,7 +990,7 @@
       rtac @{thm card1_rsp},
       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})),
-      DatatypeAux.cong_tac,
+      Cong_Tac.cong_tac @{thm cong},
       rtac @{thm ext},
 (*      rtac @{thm eq_reflection},*)
       CHANGED o (ObjectLogic.full_atomize_tac)
@@ -1232,5 +1235,5 @@
 | UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"
 *)
 
-Random test line at the end
-A second line
+end
+