test_assume_tac: now tries eq_assume_tac on exceptional cases
authorlcp
Thu Dec 08 11:28:34 1994 +0100 (1994-12-08 ago)
changeset 7621cf9ebcc3ff3
parent 761 04320c295500
child 763 d5a626aacdd3
test_assume_tac: now tries eq_assume_tac on exceptional cases
(formulae not of the form a:?A). Affects typechk_tac.
src/ZF/simpdata.ML
     1.1 --- a/src/ZF/simpdata.ML	Thu Dec 08 11:26:25 1994 +0100
     1.2 +++ b/src/ZF/simpdata.ML	Thu Dec 08 11:28:34 1994 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4  (*Try solving a:A by assumption provided a is rigid!*) 
     1.5  val test_assume_tac = SUBGOAL(fn (prem,i) =>
     1.6      if is_rigid_elem (Logic.strip_assums_concl prem)
     1.7 -    then  assume_tac i  else  no_tac);
     1.8 +    then  assume_tac i  else  eq_assume_tac i);
     1.9  
    1.10  (*Type checking solves a:?A (a rigid, ?A maybe flexible).  
    1.11    match_tac is too strict; would refuse to instantiate ?A*)