src/ZF/simpdata.ML

   | is_rigid_elem _ = false;
 
 (*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*)
 fun typechk_step_tac tyrls =
     FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);