--- a/QuotMain.thy	Tue Oct 06 11:41:35 2009 +0200
+++ b/QuotMain.thy	Tue Oct 06 11:56:23 2009 +0200
@@ -177,27 +177,26 @@
 
 ML {*
 (* tactic to prove the QUOT_TYPE theorem for the new type *)
-fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) lthy =
+fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
 let
-  val rep_thm = #Rep typedef_info
+  val unfold_mem = MetaSimplifier.rewrite_rule @{thms mem_def}
+  val rep_thm = #Rep typedef_info |> unfold_mem
   val rep_inv = #Rep_inverse typedef_info
-  val abs_inv = #Abs_inverse typedef_info
+  val abs_inv = #Abs_inverse typedef_info |> unfold_mem
   val rep_inj = #Rep_inject typedef_info
-
-  val ss = HOL_basic_ss addsimps @{thms mem_def}
-  val rep_thm_simpd = Simplifier.asm_full_simplify ss rep_thm
-  val abs_inv_simpd = Simplifier.asm_full_simplify ss abs_inv
 in
   EVERY1 [rtac @{thm QUOT_TYPE.intro},
           rtac equiv_thm,
-          rtac rep_thm_simpd,
+          rtac rep_thm,
           rtac rep_inv,
-          rtac abs_inv_simpd,
+          rtac abs_inv,
           rtac @{thm exI}, 
           rtac @{thm refl},
           rtac rep_inj]
 end
+*}
 
+ML {*
 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
 let
   val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT)
@@ -206,7 +205,7 @@
   val _ = goal |> Syntax.string_of_term lthy |> tracing
 in
   Goal.prove lthy [] [] goal
-    (K (typedef_quot_type_tac equiv_thm typedef_info lthy))
+    (K (typedef_quot_type_tac equiv_thm typedef_info))
 end