diff -r feae7b5fd425 -r 276ef51cedbf src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Apr 16 13:51:04 2004 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Apr 16 13:52:43 2004 +0200
@@ -36,11 +36,11 @@
    This makes setsum_cong more convenient to use, because assumptions
    like i:{m..n} get simplified (to m <= i & i <= n). *)
 
-ML_setup {* 
+declare setsum_cong [cong]
 
-Addcongs [thm "setsum_cong"];
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
+ML_setup {* 
+  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
+*}
 
 section {* Definition of type up *}
 
@@ -776,4 +776,4 @@
   "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
 by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero)
 
-end
\ No newline at end of file
+end