# HG changeset patch
# User paulson
# Date 1115713521 -7200
# Node ID d97c12a4f31b72c77ed879fdbc8f3e6a3f79dd34
# Parent  393cfc7184338f8456dc1f260448ef0a792bd226
oops...cannot use subst here

diff -r 393cfc718433 -r d97c12a4f31b 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)