# HG changeset patch
# User lcp
# Date 779015106 -7200
# Node ID 800603278425a22acd9a8d8ec47112ab60b4d100
# Parent  31847a7504ecbde8de2d9e29de4be6c364838088
{HOL,ZF}/indrule/quant_induct: replaced ssubst in eresolve_tac by
separate call to hyp_subst_tac.  This avoids substituting in x=f(x)

{HOL,ZF}/indrule/ind_tac: now tries resolve_tac [refl].  This handles
trivial equalities such as x=a.

{HOL,ZF}/intr_elim/intro_tacsf_tac: now calls assume_tac last, to try refl
before any equality assumptions

diff -r 31847a7504ec -r 800603278425 src/ZF/indrule.ML
--- a/src/ZF/indrule.ML	Wed Sep 07 17:28:53 1994 +0200
+++ b/src/ZF/indrule.ML	Thu Sep 08 11:05:06 1994 +0200
@@ -61,7 +61,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, iT-->oT);
@@ -75,7 +75,8 @@
       (fn prems =>
        [rtac (impI RS allI) 1,
 	etac raw_induct 1,
-	REPEAT (FIRSTGOAL (eresolve_tac [CollectE,exE,conjE,disjE,ssubst])),
+	REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE, disjE] ORELSE'
+			   hyp_subst_tac)),
 	REPEAT (FIRSTGOAL (eresolve_tac [PartE,CollectE])),
 	ind_tac (rev prems) (length prems) ]);
 
diff -r 31847a7504ec -r 800603278425 src/ZF/intr_elim.ML
--- a/src/ZF/intr_elim.ML	Wed Sep 07 17:28:53 1994 +0200
+++ b/src/ZF/intr_elim.ML	Thu Sep 08 11:05:06 1994 +0200
@@ -92,7 +92,8 @@
    REPEAT (resolve_tac [Part_eqI,CollectI] 1),
    (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
    rtac disjIn 2,
-   REPEAT (ares_tac [refl,exI,conjI] 2),
+   (*Not ares_tac, since refl must be tried before any equality assumptions*)
+   REPEAT (resolve_tac [refl,exI,conjI] 2 ORELSE assume_tac 2),
    (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
    rewrite_goals_tac con_defs,
    REPEAT (rtac refl 2),