Blast_tac now squashes flex-flex pairs immediately

--- a/src/Provers/blast.ML	Fri Jan 02 17:15:52 1998 +0100
+++ b/src/Provers/blast.ML	Fri Jan 02 17:16:39 1998 +0100
@@ -470,7 +470,7 @@
     | nNewHyps (Const "*Goal*" $ _ :: Ps) = nNewHyps Ps
     | nNewHyps (P::Ps)                    = 1 + nNewHyps Ps;
 
-  fun rot_tac [] i st      = Seq.single st
+  fun rot_tac [] i st      = Seq.single (Seq.hd (flexflex_rule st))
     | rot_tac (0::ks) i st = rot_tac ks (i+1) st
     | rot_tac (k::ks) i st = rot_tac ks (i+1) (rotate_rule (~k) i st);
 in