diff -r f8df49d4af35 -r 791b53bf4073 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Fri Dec 23 18:36:27 2005 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy	Fri Dec 23 20:02:30 2005 +0100
@@ -109,9 +109,9 @@
   done
 
 lemma subst_terms_NF: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow>
-  listall (\<lambda>t. \<forall>i j. t[Var i/j] \<in> NF) ts \<Longrightarrow>
-  listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. t[Var i/j]) ts)"
-  by (induct ts) simp+
+    listall (\<lambda>t. \<forall>i j. t[Var i/j] \<in> NF) ts \<Longrightarrow>
+    listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. t[Var i/j]) ts)"
+  by (induct ts) simp_all
 
 lemma subst_Var_NF: "t \<in> NF \<Longrightarrow> t[Var i/j] \<in> NF"
   apply (induct fixing: i j set: NF)
@@ -151,8 +151,8 @@
   done
 
 lemma lift_terms_NF: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow>
-  listall (\<lambda>t. \<forall>i. lift t i \<in> NF) ts \<Longrightarrow>
-  listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. lift t i) ts)"
+    listall (\<lambda>t. \<forall>i. lift t i \<in> NF) ts \<Longrightarrow>
+    listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. lift t i) ts)"
   by (induct ts) simp_all
 
 lemma lift_NF: "t \<in> NF \<Longrightarrow> lift t i \<in> NF"
@@ -383,8 +383,9 @@
   done
 
 
-theorem type_NF: assumes T: "e \<turnstile>\<^sub>R t : T"
-  shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" using T
+theorem type_NF:
+  assumes "e \<turnstile>\<^sub>R t : T"
+  shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" using prems
 proof induct
   case Var
   show ?case by (iprover intro: Var_NF)