# HG changeset patch
# User paulson
# Date 860056354 -7200
# Node ID fd1c0b8e9b616a19e2c0f36f3d1b35ff988602a7
# Parent  2563063772d9bc2ad6e5f02b24f9c533104b0590
Now exports declConsts!
Temporarily erased target signature to aid debugging

diff -r 2563063772d9 -r fd1c0b8e9b61 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Thu Apr 03 10:30:23 1997 +0200
+++ b/src/Provers/blast.ML	Thu Apr 03 10:32:34 1997 +0200
@@ -43,13 +43,14 @@
 signature BLAST =
   sig
   type claset
-  val depth_tac 		: claset -> int -> int -> tactic
-  val blast_tac 		: claset -> int -> tactic
-  val Blast_tac 		: int -> tactic
+  val depth_tac 	: claset -> int -> int -> tactic
+  val blast_tac 	: claset -> int -> tactic
+  val Blast_tac 	: int -> tactic
+  val declConsts 	: string list * thm list -> unit
   end;
 
 
-functor BlastFun(Data: BLAST_DATA): BLAST = 
+functor BlastFun(Data: BLAST_DATA) = 
 struct
 
 type claset = Data.claset;
@@ -138,7 +139,10 @@
 
 fun addRules (rls,tab) = foldr addConsts (map (#prop o rep_thm) rls, tab);
 
-fun declConst (a,tab) = Symtab.update((a,[]), tab);
+fun declConst (a,tab) = 
+    case Symtab.lookup (tab,a) of
+	None   => Symtab.update((a,[]), tab)	(*create a brand new entry*)
+      | Some _ => tab				(*preserve old entry*);
 
 (*maps the name of each overloaded constant to a list of archetypal constants,
   which may be polymorphic.*)
@@ -748,12 +752,12 @@
 		    handle NEWBRANCHES => 
 		     (case netMkRules G vars hazList of
 			 [] => (*no plausible rules: move G to literals*)
-			     prv (tacs, trs, choices,
+			     prv (tacs, brs0::trs, choices,
 				  (br, hazs, addLit(G,lits), vars, lim)::brs)
 		      | _ => (*G admits some haz rules: try later*)
 			     prv (if isGoal G then negOfGoal_tac :: tacs
 				  else tacs, 
-				  trs,  choices,
+				  brs0::trs,  choices,
 				  (br, addHaz((G,md),hazs), lits, vars, lim)
 				  ::brs)))
 	  end
@@ -794,7 +798,7 @@
 			  newBr (vars', dup) prems)
 		     handle PRV => 
 			 if ntrl < ntrl'       (*variables updated?*)
-			    orelse vars=vars'  (*pseudo-unsafe: no new Vars?*)
+                            orelse vars=vars'  (*pseudo-unsafe: no new Vars?*)
 			 then (*reset Vars and try another rule*)
 			      (clearTo ntrl;  deeper grls)
 			 else (*backtrack to previous level*)
@@ -814,6 +818,7 @@
  in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end;
 
 
+(*Construct an initial branch.*)
 fun initBranch (ts,lim) = 
     (map (fn t => (t,true)) ts, 
      [[]], [], add_terms_vars (ts,[]), lim);