# HG changeset patch
# User urbanc
# Date 1133696439 -3600
# Node ID b5d7649f8acac8bd4f8fda561f90b986579f1c34
# Parent  18568b35035a839c2b5421c58647a4d616658d21
tuned

diff -r 18568b35035a -r b5d7649f8aca src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Sun Dec 04 12:25:57 2005 +0100
+++ b/src/HOL/Nominal/Examples/SN.thy	Sun Dec 04 12:40:39 2005 +0100
@@ -886,5 +886,5 @@
 (* Abstractions  *)
 apply(auto dest!: t3_elim simp only: psubst_Lam)
 apply(rule abs_RED[THEN mp])
-apply(force dest: fresh_context simp add: psubs_subs)
+apply(force dest: fresh_context simp add: psubst_subst)
 done
\ No newline at end of file