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