diff -r 9be9e39fd862 -r 96fba19bcbe2 src/HOL/Integ/Group.ML
--- a/src/HOL/Integ/Group.ML	Mon Nov 03 12:12:10 1997 +0100
+++ b/src/HOL/Integ/Group.ML	Mon Nov 03 12:13:18 1997 +0100
@@ -70,7 +70,7 @@
  by (rtac plus_assoc 2);
 by (rtac trans 1);
  by (rtac plus_cong 2);
-  by (simp_tac (!simpset addsimps [left_inv,left_inv2,right_inv,right_inv2]) 2);
+  by (simp_tac (simpset() addsimps [left_inv,left_inv2,right_inv,right_inv2]) 2);
  by (rtac refl 2);
 by (rtac (zeroL RS sym) 1);
 qed "inv_plus";