# HG changeset patch
# User lcp
# Date 786882514 -3600
# Node ID 1cf9ebcc3ff379b19b60817dda29ed4130c500a4
# Parent  04320c2955006bf4ef4481a79ef1603b0a8ba94e
test_assume_tac: now tries eq_assume_tac on exceptional cases
(formulae not of the form a:?A).  Affects typechk_tac.

diff -r 04320c295500 -r 1cf9ebcc3ff3 src/ZF/simpdata.ML
--- 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*)