# HG changeset patch
# User gagern
# Date 1114029832 -7200
# Node ID 81e9f17823eac71499f182ee670911b9b2eee8d3
# Parent  ae6943098223a80393d0e4b2156544d516008f8d
Added op in front of constructor for better parsing.

diff -r ae6943098223 -r 81e9f17823ea src/Provers/blast.ML
--- 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