# HG changeset patch
# User berghofe
# Date 1120219541 -7200
# Node ID 03bdf544a552710cf00460d9955dc3201889f9de
# Parent  5a89d3622ac01c41e52273f9f143a6acc5a5c897
Removed setsubgoaler hack (thanks to strong_setsum_cong).

diff -r 5a89d3622ac0 -r 03bdf544a552 src/HOL/Algebra/poly/UnivPoly2.thy
--- 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 *}