# HG changeset patch
# User berghofe
# Date 1107364831 -3600
# Node ID 2a183ef25fb1b27fa0a3af9fa7c4c301cc4290c7
# Parent  d136af442665108feb1bfdd1f18b777eb27219b7
Replaced application of subst by simplesubst in proof of app_Var_NF
to avoid problems with program extraction.

diff -r d136af442665 -r 2a183ef25fb1 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Wed Feb 02 18:19:43 2005 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy	Wed Feb 02 18:20:31 2005 +0100
@@ -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)
   apply (rule exI)
   apply (rule conjI)
   apply (rule rtrancl_refl)