--- a/Nominal/Test.thy	Thu Mar 18 09:31:31 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 18 10:02:21 2010 +0100
@@ -61,8 +61,8 @@
 lemma
   fixes c::"'a::fs"
   assumes a1: "\<And>name c. P c (Vr name)"
-  and     a2: "\<And>lm_raw1 lm_raw2 c. \<lbrakk>\<And>d. P d lm_raw1; \<And>d. P d lm_raw2\<rbrakk> \<Longrightarrow> P c (Ap lm_raw1 lm_raw2)"
-  and     a3: "\<And>name lm_raw c. \<lbrakk>\<And>d. P d lm_raw\<rbrakk> \<Longrightarrow> P c (Lm name lm_raw)"
+  and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
+  and     a3: "\<And>name lm c. \<lbrakk>\<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
   shows "P c lm"
 proof -
   have "\<And>p. P c (p \<bullet> lm)"
@@ -73,10 +73,10 @@
     apply(rule a2)
     apply(blast)[1]
     apply(assumption)
-    apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm_raw))")
+    apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))")
     apply(erule exE)
-    apply(rule_tac t="p \<bullet> Lm name lm_raw" and 
-                   s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm_raw" in subst)
+    apply(rule_tac t="p \<bullet> Lm name lm" and 
+                   s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst)
     apply(simp)
     apply(subst lm_perm)
     apply(subst (2) lm_perm)
@@ -90,7 +90,7 @@
     apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec)
     apply(simp)
     apply(simp add: fresh_def)
-    apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm_raw))" in obtain_at_base)
+    apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base)
     apply(simp add: supp_Pair finite_supp)
     apply(blast)
     done