# HG changeset patch
# User paulson
# Date 877079556 -7200
# Node ID 6ea5f9101c3e84ddafefb515bc4bc3e873edc160
# Parent  be9ae8de1615e16a4ad6cb62f225ea59c15cf2b8
A lot of new comments

diff -r be9ae8de1615 -r 6ea5f9101c3e src/Provers/blast.ML
--- a/src/Provers/blast.ML	Fri Oct 17 11:10:54 1997 +0200
+++ b/src/Provers/blast.ML	Fri Oct 17 11:12:36 1997 +0200
@@ -364,6 +364,8 @@
 
 
 (*First-order unification with bound variables.  
+  "allowClash", if true, treats OConst and Const as the same;
+	we do so when closing a branch but not when applying rules!
   "vars" is a list of variables local to the rule and NOT to be put
 	on the trail (no point in doing so)
 *)
@@ -848,6 +850,8 @@
      fun prv (tacs, trs, choices, []) = cont (tacs, trs, choices)
        | prv (tacs, trs, choices, 
 	      brs0 as (((G,md)::br, haz)::pairs, lits, vars, lim) :: brs) =
+   	     (*apply a safe rule only (possibly allowing instantiation);
+               defer any haz formulae*)
 	  let exception PRV (*backtrack to precisely this recursion!*)
 	      val ntrl = !ntrail 
 	      val nbrs = length brs0
@@ -941,7 +945,7 @@
 		 deeper rules
 		  handle NEWBRANCHES => 
 		   (case netMkRules G vars hazList of
-		       [] => (*no plausible rules: move G to literals*)
+		       [] => (*no plausible haz rules: move G to literals*)
 			   prv (tacs, brs0::trs, choices,
 				((br,haz)::pairs, addLit(G,lits), vars, lim)
 				::brs)
@@ -992,9 +996,18 @@
 				   both dup and recur are false.  Proofs are
 				   found at shallower depths, but looping
 				   occurs too often...*)
-			 val mayUndo = not(null grls)   (*other rules to try?*)
-				     orelse ntrl < ntrl' (*variables updated?*)
-				     orelse vars=vars'   (*no new Vars?*)
+			 val mayUndo = 
+			     (*Allowing backtracking from a rule application
+			       if other matching rules exist, if the rule
+			       updated variables, or if the rule did not
+			       introduce new variables.  This latter condition
+			       means it is not a standard "gamma-rule" but
+			       some other form of unsafe rule.  Aim is to
+			       emulate Fast_tac, which allows all unsafe steps
+			       to be undone.*)
+			     not(null grls)   (*other rules to try?*)
+			     orelse ntrl < ntrl' (*variables updated?*)
+			     orelse vars=vars'   (*no new Vars?*)
 			 val tac' = if mayUndo then tac dup
 				    else DETERM o (tac dup) 
 		     in