--- 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;