Replaced !simpset by HOL_ss on line 93.
authornipkow
Thu, 04 Apr 1996 20:13:46 +0200
changeset 1653 1a2ffa2fbf7d
parent 1652 9b78ce58d6b1
child 1654 faa643c33ee6
Replaced !simpset by HOL_ss on line 93.
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)])