diff -r 38e5c05ef741 -r 5a3e336a2e37 src/HOL/Complex/ex/ReflectedFerrack.thy
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -1908,7 +1908,7 @@
   from alluopairs_set1[where xs="?U"] have UpU: "set ?Up \<le> (set ?U \<times> set ?U)" by simp
   from uset_l[OF lq] have U_l: "\<forall> (t,n) \<in> set ?U. numbound0 t \<and> n > 0" .
   from U_l UpU 
-  have Up_: "\<forall> ((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" by auto
+  have "\<forall> ((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" by auto
   hence Snb: "\<forall> (t,n) \<in> set ?S. numbound0 t \<and> n > 0 "
     by (auto simp add: mult_pos_pos)
   have Y_l: "\<forall> (t,n) \<in> set ?Y. numbound0 t \<and> n > 0"