src/HOL/indrule.ML
changeset 1653 1a2ffa2fbf7d
parent 1465 5d7a7e439cec
child 1728 01beef6262aa
--- 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)])