test_assume_tac: now tries eq_assume_tac on exceptional cases
(formulae not of the form a:?A). Affects typechk_tac.
--- a/src/ZF/simpdata.ML Thu Dec 08 11:26:25 1994 +0100
+++ b/src/ZF/simpdata.ML Thu Dec 08 11:28:34 1994 +0100
@@ -15,7 +15,7 @@
(*Try solving a:A by assumption provided a is rigid!*)
val test_assume_tac = SUBGOAL(fn (prem,i) =>
if is_rigid_elem (Logic.strip_assums_concl prem)
- then assume_tac i else no_tac);
+ then assume_tac i else eq_assume_tac i);
(*Type checking solves a:?A (a rigid, ?A maybe flexible).
match_tac is too strict; would refuse to instantiate ?A*)