--- a/src/Provers/blast.ML Fri Sep 11 16:26:22 1998 +0200
+++ b/src/Provers/blast.ML Fri Sep 11 16:31:40 1998 +0200
@@ -1125,8 +1125,7 @@
not(null grls) (*other rules to try?*)
orelse updated
orelse vars=vars' (*no new Vars?*)
- val tac' = if mayUndo then tac(updated, dup, true)
- else DETERM o tac(updated, dup, true)
+ val tac' = tac(updated, dup, true)
(*if recur then perhaps shouldn't call rotate_tac: new
formulae should be last, but that's WRONG if the new
formulae are Goals, since they remain in the first