# HG changeset patch
# User urbanc
# Date 1133361008 -3600
# Node ID 0c5c3b1a700e04f8b0b43faf4806113c55e6c4a7
# Parent  ca1ac9e81bc86f5f05ed1d5c8808834fd95a7ede
fixed the lemma where the new names generated by nominal_induct
caused problems.

diff -r ca1ac9e81bc8 -r 0c5c3b1a700e src/HOL/Nominal/Examples/Lam_substs.thy
--- a/src/HOL/Nominal/Examples/Lam_substs.thy	Wed Nov 30 15:27:30 2005 +0100
+++ b/src/HOL/Nominal/Examples/Lam_substs.thy	Wed Nov 30 15:30:08 2005 +0100
@@ -1372,10 +1372,10 @@
   and   t1:: "lam"
   and   t2:: "lam"
   and   a :: "name"
-  shows "pi\<bullet>(t1[a::=t2]) = (pi\<bullet>t1)[(pi\<bullet>a)::=(pi\<bullet>t2)]"
-apply(nominal_induct t1 fresh: a t2 rule: lam_induct)
+  shows "pi\<bullet>(t1[b::=t2]) = (pi\<bullet>t1)[(pi\<bullet>b)::=(pi\<bullet>t2)]"
+apply(nominal_induct t1 fresh: b t2 rule: lam_induct)
 apply(auto simp add: perm_bij fresh_prod fresh_atm)
-apply(subgoal_tac "(pi\<bullet>a)\<sharp>(pi\<bullet>b,pi\<bullet>ba)")(*A*)
+apply(subgoal_tac "(pi\<bullet>a)\<sharp>(pi\<bullet>b,pi\<bullet>t2)")(*A*)
 apply(simp) 
 apply(simp add: perm_bij fresh_prod fresh_atm pt_fresh_bij[OF pt_name_inst, OF at_name_inst]) 
 done