diff -r 5a9bdf81672d -r 3f3927f793d4 LFex.thy
--- a/LFex.thy	Fri Nov 27 07:16:16 2009 +0100
+++ b/LFex.thy	Fri Nov 27 08:15:23 2009 +0100
@@ -180,12 +180,6 @@
 where
   "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
 
-ML {* val defs =
-  @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def
-    FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def}
-*}
-ML {* val consts = lookup_quot_consts defs *}
-
 thm akind_aty_atrm.induct
 
 lemma left_ball_regular:
@@ -279,6 +273,10 @@
   end
 *}
 
+ML {* val defs =
+  @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def
+    FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def}
+*}
 
 lemma "\<lbrakk>P1 TYP TYP; \<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x K');
  \<And>A A' K x x' K'.
@@ -301,8 +299,15 @@
 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
 prefer 2
-apply(tactic {* r_mk_comb_tac' @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply (tactic {* clean_tac @{context} quot defs reps_same absrep 1 *})
+thm QUOTIENT_TY
+apply (tactic {* clean_tac @{context} @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} defs [] 1 *})
+
+
+print_quotients
+apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl trans2 [] 1*})
+
+
+ML {* val consts = lookup_quot_consts defs *}
 
 ML {*
 val rty_qty_rel =