changeset 22678 | 23963361278c |
parent 22596 | d0d2af4db18f |
child 23591 | d32a85385e17 |
--- a/src/Provers/blast.ML Sat Apr 14 17:36:03 2007 +0200 +++ b/src/Provers/blast.ML Sat Apr 14 17:36:05 2007 +0200 @@ -1212,7 +1212,7 @@ | SOME(v,is) => if is=bounds ts then Var v else raise TRANS ("Discrepancy among occurrences of " - ^ Syntax.string_of_vname ix)) + ^ Term.string_of_vname ix)) | Term.Abs (a,_,body) => if null ts then Abs(a, from (lev+1) body) else raise TRANS "argument not in normal form"