--- a/LFex.thy	Mon Nov 30 10:16:10 2009 +0100
+++ b/LFex.thy	Mon Nov 30 11:53:20 2009 +0100
@@ -492,6 +492,21 @@
 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
 done
 
+(* Does not work:
+lemma
+  assumes a0: "P1 TYP"
+  and     a1: "\<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind)"
+  and     a2: "\<And>id. P2 (TCONST id)"
+  and     a3: "\<And>ty trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P2 (TAPP ty trm)"
+  and     a4: "\<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2)"
+  and     a5: "\<And>id. P3 (CONS id)"
+  and     a6: "\<And>name. P3 (VAR name)"
+  and     a7: "\<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2)"
+  and     a8: "\<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)"
+  shows "P1 mkind \<and> P2 mty \<and> P3 mtrm"
+using a0 a1 a2 a3 a4 a5 a6 a7 a8
+*)
+
 lemma "\<lbrakk>P1 TYP;
   \<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind);
   \<And>id. P2 (TCONST id);
@@ -501,6 +516,7 @@
   \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2);
   \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk>
   \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm"
+
 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm kind_ty_trm.induct})) (term_of qtm) *}