author | nipkow |
Thu, 04 Apr 1996 20:13:46 +0200 | |
changeset 1653 | 1a2ffa2fbf7d |
parent 1652 | 9b78ce58d6b1 |
child 1654 | faa643c33ee6 |
--- 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)])