diff -r d00dd828f7af -r 2922b04d9545 Nominal/ExCoreHaskell.thy
--- a/Nominal/ExCoreHaskell.thy	Fri Mar 26 22:23:22 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy	Sat Mar 27 06:44:14 2010 +0100
@@ -312,7 +312,7 @@
 apply (simp)
 oops
 
-lemma 
+lemma strong_inudction_principle:
   assumes a01: "\<And>b. P1 b KStar"
   and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"
   and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)"