src/Provers/blast.ML

 				    Int.toString lim);
 			   backtrack choices)
 		| cell => Sequence.seqof(fn()=> cell))
      in prove (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], cont)
      end
-     handle Subscript => Sequence.null
-	  | PROVE     => Sequence.null);
+     handle PROVE     => Sequence.null);
 
 fun blast_tac cs = (DEEPEN (1,20) (depth_tac cs) 0);
 
 fun Blast_tac i = blast_tac (!Data.claset) i;