--- a/src/Pure/term.ML Tue Oct 21 17:38:31 1997 +0200+++ b/src/Pure/term.ML Tue Oct 21 17:47:50 1997 +0200@@ -50,7 +50,7 @@ | Var of indexname * typ | Bound of int | Abs of string*typ*term- | $ of term*term;+ | op $ of term*term; (*For errors involving type mismatches*)