src/Provers/blast.ML
changeset 15786 81e9f17823ea
parent 15661 9ef583b08647
child 16774 515b6020cf5d
--- a/src/Provers/blast.ML	Wed Apr 20 22:37:29 2005 +0200
+++ b/src/Provers/blast.ML	Wed Apr 20 22:43:52 2005 +0200
@@ -77,7 +77,7 @@
     | 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