src/Provers/blast.ML

     | Skolem of string * term option ref list
     | Free  of string
     | Var   of term option ref
     | Bound of int
     | Abs   of string*term
-    | op $  of term*term;
+    | $  of term*term;
   type branch
   val depth_tac 	: claset -> int -> int -> tactic
   val depth_limit : int ref
   val blast_tac 	: claset -> int -> tactic
   val Blast_tac 	: int -> tactic

 (*nbrs = # of branches just prior to closing this one.  Delete choice points
   for goals proved by the latest inference, provided NO variables in the
   next branch have been updated.*)
 fun prune (1, nxtVars, choices) = choices  (*DON'T prune at very end: allow 
 					     backtracking over bad proofs*)
-  | prune (nbrs, nxtVars, choices) =
+  | prune (nbrs: int, nxtVars, choices) =
       let fun traceIt last =
 		let val ll = length last
 		    and lc = length choices
 		in if !trace andalso ll<lc then
 		    (writeln("Pruning " ^ Int.toString(lc-ll) ^ " levels");