diff -r 9be9e39fd862 -r 96fba19bcbe2 src/HOL/Integ/Ring.ML
--- a/src/HOL/Integ/Ring.ML	Mon Nov 03 12:12:10 1997 +0100
+++ b/src/HOL/Integ/Ring.ML	Mon Nov 03 12:13:18 1997 +0100
@@ -141,7 +141,7 @@
 (*** The order [minus_plusL3,minus_plusL2] is important because minus_plusL3
      MUST be tried first ***)
 val cring_simp =
-  let val phase1 = !simpset addsimps
+  let val phase1 = simpset() addsimps
                    [plus_minusL,minus_plusR,minus_minusR,plus_minusR]
       val phase2 = HOL_ss addsimps [minus_plusL3,minus_plusL2,
                                     zeroL,zeroR,mult_zeroL,mult_zeroR]