Removed setsubgoaler hack (thanks to strong_setsum_cong).

--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Jul 01 14:03:50 2005 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Jul 01 14:05:41 2005 +0200
@@ -34,15 +34,10 @@
 qed
 *)
 
-(* Instruct simplifier to simplify assumptions introduced by congs.
-   This makes setsum_cong more convenient to use, because assumptions
+(* With this variant of setsum_cong, assumptions
    like i:{m..n} get simplified (to m <= i & i <= n). *)
 
-declare setsum_cong [cong]
-
-ML_setup {* 
-  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
-*}
+declare strong_setsum_cong [cong]
 
 section {* Definition of type up *}