# HG changeset patch
# User paulson
# Date 905524300 -7200
# Node ID c41956742c2eca38c679eaee6096092c82d75c12
# Parent  93c21fee39f81b0f3c8256cbfb172905bb2d8083
Less deterministic reconstruction: now more robust but perhaps slower

diff -r 93c21fee39f8 -r c41956742c2e src/Provers/blast.ML
--- 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