MLWorks demands the "op" before $
authorpaulson
Mon, 05 Oct 1998 10:30:57 +0200
changeset 5613 5cb6129566e7
parent 5612 e981ca6f7332
child 5614 0e8b45a7d104
MLWorks demands the "op" before $
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 **)