# HG changeset patch
# User paulson
# Date 907576257 -7200
# Node ID 5cb6129566e755ffeb75d8659dce62a27acd214f
# Parent  e981ca6f733259730700506e23e0fe4c60528cd9
MLWorks demands the "op" before $

diff -r e981ca6f7332 -r 5cb6129566e7 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Mon Oct 05 10:27:04 1998 +0200
+++ b/src/Provers/blast.ML	Mon Oct 05 10:30:57 1998 +0200
@@ -123,7 +123,7 @@
   | Var    of term option ref
   | Bound  of int
   | Abs    of string*term
-  | $      of term*term;
+  | op $   of term*term;
 
 
 (** Basic syntactic operations **)