# HG changeset patch
# User urbanc
# Date 1137548938 -3600
# Node ID 13e11abcfc96f00dbc9f27660d23597cf2d438f6
# Parent  7dc7dcd63224c758c7ea0b946fe371400863635d
fixed one proof that broke because of the changes
Markus did on the rules ex1I

diff -r 7dc7dcd63224 -r 13e11abcfc96 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Tue Jan 17 16:36:57 2006 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Wed Jan 18 02:48:58 2006 +0100
@@ -2007,7 +2007,7 @@
   and     f1: "finite ((supp h)::'x set)"
   and     a: "\<exists>(a::'x). (a\<sharp>h \<and> a\<sharp>(h a))"
   shows  "\<exists>!(fr::'a). \<forall>(a::'x). a\<sharp>h \<longrightarrow> (h a) = fr"
-proof
+proof (rule ex_ex1I)
   from pt at f1 a show "\<exists>fr::'a. \<forall>a::'x. a\<sharp>h \<longrightarrow> h a = fr" by (simp add: freshness_lemma)
 next
   fix fr1 fr2
@@ -2640,10 +2640,10 @@
 
 method_setup supports_simp =
   {* supports_meth *}
-  {* tactic for deciding whether something supports semthing else *}
+  {* tactic for deciding whether something supports something else *}
 
 method_setup supports_simp_debug =
   {* supports_meth_debug *}
-  {* tactic for deciding equalities involving permutations including debuging facilities *}
+  {* tactic for deciding whether something supports something else including debuging facilities *}
 
 end