diff -r 9b78ce58d6b1 -r 1a2ffa2fbf7d src/HOL/indrule.ML
--- a/src/HOL/indrule.ML	Thu Apr 04 18:18:48 1996 +0200
+++ b/src/HOL/indrule.ML	Thu Apr 04 20:13:46 1996 +0200
@@ -90,7 +90,7 @@
       (fn prems =>
        [rtac (impI RS allI) 1,
         DETERM (etac Intr_elim.raw_induct 1),
-        asm_full_simp_tac (!simpset addsimps [Part_Collect]) 1,
+        asm_full_simp_tac (HOL_ss addsimps [Part_Collect]) 1,
         REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE] 
                            ORELSE' hyp_subst_tac)),
         ind_tac (rev prems) (length prems)])