--- a/FSet.thy	Mon Nov 02 09:47:49 2009 +0100
+++ b/FSet.thy	Mon Nov 02 11:15:26 2009 +0100
@@ -343,12 +343,17 @@
   apply (atomize(full))
   apply (tactic {* tac @{context} 1 *}) *)
 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv rel_refl @{context} *}
-ML {*
+(* ML {*
   val rt = build_repabs_term @{context} ind_r_r consts rty qty
   val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt);
 *}
-(*prove rg
+prove rg
 apply(atomize(full))
+ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
+apply (tactic {*  (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {*  (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {*  (r_mk_comb_tac_fset @{context}) 1 *})
+
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 done*)
 ML {* val ind_r_t =

--- a/LamEx.thy	Mon Nov 02 09:47:49 2009 +0100
+++ b/LamEx.thy	Mon Nov 02 11:15:26 2009 +0100
@@ -240,6 +240,75 @@
  *}
   apply (tactic {* tac @{context} 1 *}) *)
 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
+ML {*
+  val rt = build_repabs_term @{context} t_r consts rty qty
+  val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
+*}
+prove rg
+apply(atomize(full))
+ML_prf {*
+fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
+  (FIRST' [
+    rtac trans_thm,
+    LAMBDA_RES_TAC ctxt,
+    res_forall_rsp_tac ctxt,
+    res_exists_rsp_tac ctxt,
+    (
+     (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms))
+     THEN_ALL_NEW (fn _ => no_tac)
+    ),
+    (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
+    rtac refl,
+(*    rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*)
+    (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
+    Cong_Tac.cong_tac @{thm cong},
+    rtac @{thm ext},
+    rtac reflex_thm,
+    atac,
+    (
+     (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+     THEN_ALL_NEW (fn _ => no_tac)
+    ),
+    WEAK_LAMBDA_RES_TAC ctxt
+    ]);
+  fun r_mk_comb_tac_lam lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms
+*}
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+prefer 2
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+
+
 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
 
 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *}

--- a/QuotMain.thy	Mon Nov 02 09:47:49 2009 +0100
+++ b/QuotMain.thy	Mon Nov 02 11:15:26 2009 +0100
@@ -416,8 +416,11 @@
 text {* tyRel takes a type and builds a relation that a quantifier over this
   type needs to respect. *}
 ML {*
+fun matches (ty1, ty2) =
+  Type.raw_instance (ty1, Logic.varifyT ty2);
+
 fun tyRel ty rty rel lthy =
-  if ty = rty 
+  if matches (rty, ty)
   then rel
   else (case ty of
           Type (s, tys) =>
@@ -892,8 +895,8 @@
 ML {*
 fun lookup_quot_data lthy qty =
   let
-    val SOME quotdata = find_first (fn x => #qtyp x = qty) (quotdata_lookup lthy)
-    val rty = #rtyp quotdata
+    val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy)
+    val rty = Logic.unvarifyT (#rtyp quotdata)
     val rel = #rel quotdata
     val rel_eqv = #equiv_thm quotdata
     val rel_refl_pre = @{thm EQUIV_REFL} OF [rel_eqv]