# HG changeset patch
# User wenzelm
# Date 1343420580 -7200
# Node ID 3c4d7ff75f010e24a39f458734e73213d305b59c
# Parent  6e57023954917569545aa69e21ccbd5eff4f7132
tuned proofs -- avoid odd situations of polymorphic Frees in goal state;

diff -r 6e5702395491 -r 3c4d7ff75f01 src/HOL/Nominal/Examples/Class1.thy
--- 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)