# HG changeset patch
# User urbanc
# Date 1138025646 -3600
# Node ID e8a11e84864cf5c7adeff64aaf39f1778c9156bd
# Parent  f0d901bc0686780199b1f87407ad33b9c28aea59
made change for ex1

diff -r f0d901bc0686 -r e8a11e84864c src/HOL/Nominal/Examples/Lam_substs.thy
--- 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