Tuned.

--- a/src/HOL/Lambda/WeakNorm.thy	Tue Jun 01 11:13:09 2010 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Tue Jun 01 11:13:40 2010 +0200
@@ -264,6 +264,7 @@
 lemmas [extraction_expand] = conj_assoc listall_cons_eq
 
 extract type_NF
+
 lemma rtranclR_rtrancl_eq: "rtranclpR r a b = r\<^sup>*\<^sup>* a b"
   apply (rule iffI)
   apply (erule rtranclpR.induct)