tuned proofs -- avoid odd situations of polymorphic Frees in goal state;

--- a/src/HOL/Nominal/Examples/Class1.thy	Fri Jul 27 21:57:56 2012 +0200
+++ b/src/HOL/Nominal/Examples/Class1.thy	Fri Jul 27 22:23:00 2012 +0200
@@ -6791,7 +6791,7 @@
     apply(force)
     apply(rule exists_fresh'(1)[OF fs_name1])
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,Ax y c,M{x2:=<c>.Ax y c},M{x2:=<c>.Ax y c}{y:=<c>.P},
-                                        M'{x2:=<c>.Ax y c},M'{x2:=<c>.Ax y c}{y:=<c>.P},x1,x2,x3,y,x)")
+                                        M'{x2:=<c>.Ax y c},M'{x2:=<c>.Ax y c}{y:=<c>.P},x1,x2,y,x)")
     apply(erule exE, simp only: fresh_prod)
     apply(erule conjE)+
     apply(simp only: fresh_fun_simp_ImpL)