made change for ex1

--- a/src/HOL/Nominal/Examples/Lam_substs.thy	Mon Jan 23 14:07:52 2006 +0100
+++ b/src/HOL/Nominal/Examples/Lam_substs.thy	Mon Jan 23 15:14:06 2006 +0100
@@ -567,7 +567,7 @@
   assumes f: "finite ((supp (f1,f2,f3))::name set)"
   and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
   shows "\<exists>!y. (t,y)\<in>rec f1 f2 f3"
-proof 
+proof (rule ex_ex1I)
   case goal1
   show ?case by (rule rec_total[OF f, OF c])
 next