src/HOL/Lambda/WeakNorm.thy

--- a/src/HOL/Lambda/WeakNorm.thy	Tue May 10 06:59:32 2005 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Tue May 10 10:25:21 2005 +0200
@@ -134,7 +134,7 @@
 
 lemma app_Var_NF: "t \<in> NF \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"
   apply (induct set: NF)
-  apply (subst app_last)
+  apply (simplesubst app_last)  --{*Using @{text subst} makes extraction fail*}
   apply (rule exI)
   apply (rule conjI)
   apply (rule rtrancl_refl)