fixed the lemma where the new names generated by nominal_induct
caused problems.
--- 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