diff -r 96c68fd7ed46 -r f745ff8bdb91 indrule.ML --- a/indrule.ML Wed Sep 07 13:17:34 1994 +0200 +++ b/indrule.ML Thu Sep 08 11:01:45 1994 +0200 @@ -68,7 +68,7 @@ (*Avoids backtracking by delivering the correct premise to each goal*) fun ind_tac [] 0 = all_tac - | ind_tac(prem::prems) i = REPEAT (ares_tac [Part_eqI,prem] i) THEN + | ind_tac(prem::prems) i = REPEAT (ares_tac [Part_eqI, prem, refl] i) THEN ind_tac prems (i-1); val pred = Free(pred_name, elem_type --> boolT); @@ -82,8 +82,8 @@ (fn prems => [rtac (impI RS allI) 1, etac raw_induct 1, - REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE, - ssubst])), + REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE] + ORELSE' hyp_subst_tac)), REPEAT (FIRSTGOAL (eresolve_tac [PartE, CollectE])), ind_tac (rev prems) (length prems)]) handle e => print_sign_exn sign e; @@ -128,7 +128,7 @@ (fn prems => [cut_facts_tac prems 1, REPEAT (eresolve_tac [asm_rl, conjE, PartE, mp] 1 - ORELSE resolve_tac [allI, impI, conjI, Part_eqI] 1 + ORELSE resolve_tac [allI, impI, conjI, Part_eqI, refl] 1 ORELSE dresolve_tac [spec, mp, splitD] 1)]) handle e => print_sign_exn sign e;