--- a/LFex.thy	Mon Nov 09 13:47:46 2009 +0100
+++ b/LFex.thy	Mon Nov 09 15:23:33 2009 +0100
@@ -180,6 +180,37 @@
 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
+
+ML {*
+val rty_qty_rel =
+  [(@{typ kind}, (@{typ KIND}, @{term akind})),
+   (@{typ ty}, (@{typ TY}, @{term aty})),
+   (@{typ trm}, (@{typ TRM}, @{term atrm}))]
+*}
+
+print_quotients
+
+ML {* val rty = [@{typ }]
+ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *}
+ML {* val t_a = atomize_thm @{thm akind_aty_atrm.induct} *}
+prove {* build_regularize_goal t_a rty rel @{context}
+
 end