# HG changeset patch
# User wenzelm
# Date 1208202293 -7200
# Node ID 147c920ed5f784f331f3d7d4f7bda73161625495
# Parent  540ad65e804c266e45a179fb0f548106009f1e4c
avoid duplicate fact bindings;

diff -r 540ad65e804c -r 147c920ed5f7 src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Mon Apr 14 21:44:51 2008 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Mon Apr 14 21:44:53 2008 +0200
@@ -458,7 +458,7 @@
 apply(perm_simp)
 done
 
-lemma test2:
+lemma test2b:
   assumes a: "x\<sharp>(\<Gamma>,s,t) \<and> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^isub>2"
   shows "\<forall>x. x\<sharp>\<Gamma> \<longrightarrow> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^isub>2"
 using a