--- a/IntEx.thy	Thu Nov 05 09:38:34 2009 +0100
+++ b/IntEx.thy	Thu Nov 05 09:55:21 2009 +0100
@@ -158,7 +158,8 @@
 ML {* val consts = lookup_quot_consts defs *}
 ML {* val t_a = atomize_thm @{thm ho_tst} *}
 
-(*prove t_r: {* build_regularize_goal t_a rty rel @{context} *}
+(*
+prove t_r: {* build_regularize_goal t_a rty rel @{context} *}
 ML_prf {*   fun tac ctxt =
       (ObjectLogic.full_atomize_tac) THEN'
      REPEAT_ALL_NEW (FIRST' [
@@ -183,6 +184,7 @@
   val rt = build_repabs_term @{context} t_r consts rty qty
   val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
 *}
+*)
 
 lemma foldl_rsp:
   "((IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel) ===>

--- a/LamEx.thy	Thu Nov 05 09:38:34 2009 +0100
+++ b/LamEx.thy	Thu Nov 05 09:55:21 2009 +0100
@@ -33,16 +33,26 @@
 print_theorems
 
 lemma alpha_refl:
-  shows "x \<approx> x"
-  apply (rule rlam.induct)
-  apply (simp_all add:a1 a2)
-  apply (rule a3)
-  apply (simp_all)
-  (* apply (simp add: pt_swap_bij'') *)
+  fixes t::"rlam"
+  shows "t \<approx> t"
+  apply(induct t rule: rlam.induct)
+  apply(simp add: a1)
+  apply(simp add: a2)
+  apply(rule a3)
+  apply(subst pt_swap_bij'')
+  apply(rule pt_name_inst)
+  apply(rule at_name_inst)
+  apply(simp)
+  apply(simp)
+  done
+
+lemma alpha_EQUIV:
+  shows "EQUIV alpha"
 sorry
 
 quotient lam = rlam / alpha
-sorry
+  apply(rule alpha_EQUIV)
+  done
 
 print_quotients
 
@@ -126,12 +136,14 @@
   shows "Lam a t = Lam b s"
 sorry
 
-lemma perm_rsp: "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>"
+lemma perm_rsp: 
+  "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>"
   apply(auto)
   (* this is propably true if some type conditions are imposed ;o) *)
   sorry
 
-lemma fresh_rsp: "(op = ===> alpha ===> op =) fresh fresh" 
+lemma fresh_rsp: 
+  "(op = ===> alpha ===> op =) fresh fresh" 
   apply(auto)
   (* this is probably only true if some type conditions are imposed *)
   sorry
@@ -190,6 +202,10 @@
 ML {* val a2 = lift_thm_lam @{context} @{thm a2} *}
 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *}
 
+thm a2
+ML {* val t_a = atomize_thm @{thm a2} *}
+ML {* val t_r = regularize t_a @{typ rlam} @{term alpha} @{thm alpha_EQUIV} @{thm alpha_refl} @{context} *}
+
 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *}
 ML {* val alpha_induct = lift_thm_lam @{context} @{thm alpha.induct} *}
 

--- a/QuotMain.thy	Thu Nov 05 09:38:34 2009 +0100
+++ b/QuotMain.thy	Thu Nov 05 09:55:21 2009 +0100
@@ -171,38 +171,6 @@
 
 section {* ATOMIZE *}
 
-text {*
-  Unabs_def converts a definition given as
-
-    c \<equiv> %x. %y. f x y
-
-  to a theorem of the form
-
-    c x y \<equiv> f x y
-
-  This function is needed to rewrite the right-hand
-  side to the left-hand side.
-*}
-
-ML {*
-fun unabs_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
-
-  val thy = ProofContext.theory_of ctxt'
-  val cxs = map (cterm_of thy o Free) xs
-  val new_lhs = Drule.list_comb (lhs, cxs)
-
-  fun get_conv [] = Conv.rewr_conv def
-    | get_conv (x::xs) = Conv.fun_conv (get_conv xs)
-in
-  get_conv xs new_lhs |>
-  singleton (ProofContext.export ctxt' ctxt)
-end
-*}
-
 lemma atomize_eqv[atomize]: 
   shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" 
 proof

--- a/quotient_def.ML	Thu Nov 05 09:38:34 2009 +0100
+++ b/quotient_def.ML	Thu Nov 05 09:55:21 2009 +0100
@@ -128,7 +128,7 @@
 
 fun sanity_chk lthy qenv =
 let
-  val qenv' = Quotient_Info.mk_qenv lthy
+  val global_qenv = Quotient_Info.mk_qenv lthy
   val thy = ProofContext.theory_of lthy
 
   fun is_inst thy (qty, rty) (qty', rty') =
@@ -141,7 +141,8 @@
   else false
 
   fun chk_inst (qty, rty) = 
-    if exists (is_inst thy (qty, rty)) qenv' then true
+    if exists (is_inst thy (qty, rty)) global_qenv 
+    then true
     else error_msg lthy (qty, rty)
 in
   forall chk_inst qenv