--- a/QuotMain.thy	Mon Oct 05 11:54:02 2009 +0200
+++ b/QuotMain.thy	Tue Oct 06 01:50:13 2009 +0200
@@ -177,7 +177,7 @@
 
 ML {*
 (* tactic to prove the QUOT_TYPE theorem for the new type *)
-fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
+fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) lthy =
 let
   val rep_thm = #Rep typedef_info
   val rep_inv = #Rep_inverse typedef_info
@@ -192,19 +192,21 @@
           rtac equiv_thm,
           rtac rep_thm_simpd,
           rtac rep_inv,
-          rtac abs_inv_simpd, rtac @{thm exI}, rtac @{thm refl},
+          rtac abs_inv_simpd,
+          rtac @{thm exI}, 
+          rtac @{thm refl},
           rtac rep_inj]
 end
 
-
 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
 let
   val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT)
   val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
              |> Syntax.check_term lthy
+  val _ = goal |> Syntax.string_of_term lthy |> tracing
 in
   Goal.prove lthy [] [] goal
-    (K (typedef_quot_type_tac equiv_thm typedef_info))
+    (K (typedef_quot_type_tac equiv_thm typedef_info lthy))
 end
 
 
@@ -730,21 +732,24 @@
 *}
 
 ML {*
-fun unlam_def_aux orig_ctxt ctxt t =
-  let val rhs = Thm.rhs_of t in
-  (case try (Thm.dest_abs NONE) rhs of
-    SOME (v, vt) =>
-      let
-        val (vname, vt) = Term.dest_Free (Thm.term_of v)
-        val ([vnname], ctxt) = Variable.variant_fixes [vname] ctxt
-        val nv = Free(vnname, vt)
-        val t2 = Drule.fun_cong_rule t (Thm.cterm_of (ProofContext.theory_of ctxt) nv)
-        val tnorm = equal_elim (Drule.beta_eta_conversion (Thm.cprop_of t2)) t2
-      in unlam_def_aux orig_ctxt ctxt tnorm end
-  | NONE => singleton (ProofContext.export ctxt orig_ctxt) t)
-  end;
+fun unlam_def ctxt def =
+let
+  val (lhs, rhs) = Thm.dest_equals (cprop_of def)
+  val xs = strip_abs_vars (term_of rhs)
+  val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt
 
-fun unlam_def ctxt t = unlam_def_aux ctxt ctxt t
+  fun get_lhs [] = lhs
+    | get_lhs (x::xs) =  
+        let val cx = cterm_of (ProofContext.theory_of ctxt') (Free x)
+        in Thm.capply (get_lhs xs) cx end
+
+  fun get_conv [] = Conv.rewr_conv def
+    | get_conv (x::xs) = Conv.fun_conv (get_conv xs)
+ 
+in
+  get_conv xs (get_lhs (rev xs)) |>  
+  singleton (ProofContext.export ctxt' ctxt)
+end
 *}
 
 local_setup {*
@@ -754,6 +759,9 @@
 term membship
 term IN
 thm IN_def
+ML {* (Conv.fun_conv (Conv.fun_conv (Conv.rewr_conv @{thm IN_def}))) @{cterm "IN x y"}*}
+ML {* MetaSimplifier.rewrite_rule @{thms IN_def} @{thm IN_def}*}
+
 ML {* unlam_def @{context} @{thm IN_def} *}
 
 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset]