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
-    | $  of term*term;
+    | op $  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