author | gagern |
Wed, 20 Apr 2005 22:43:52 +0200 | |
changeset 15786 | 81e9f17823ea |
parent 15785 | ae6943098223 |
child 15787 | 8fad4bd4e53c |
--- 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