src/Provers/blast.ML
changeset 5411 7a43b484f6d2
parent 5343 871b77df79a0
child 5463 a5479f5cd482
--- a/src/Provers/blast.ML	Tue Sep 01 10:10:11 1998 +0200
+++ b/src/Provers/blast.ML	Tue Sep 01 10:10:27 1998 +0200
@@ -1196,7 +1196,7 @@
 				Var (hdvar(!alistVar)))
 		     | Some(v,is) => if is=bounds ts then Var v
 			    else raise TRANS
-				("Discrepancy among occurrences of ?"
+				("Discrepancy among occurrences of "
 				 ^ Syntax.string_of_vname ix))
 	    | Term.Abs (a,_,body) => 
 		  if null ts then Abs(a, from (lev+1) body)