# HG changeset patch # User wenzelm # Date 861357314 -7200 # Node ID 8189a4870d196f6a2cfb988e1af681fed2731c6e # Parent d38f330e58b324f925fd57c919385ecdd4caa4f9 tuned err msg; diff -r d38f330e58b3 -r 8189a4870d19 src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML Fri Apr 18 11:54:54 1997 +0200 +++ b/src/Pure/type_infer.ML Fri Apr 18 11:55:14 1997 +0200 @@ -257,7 +257,7 @@ (* adjust sorts of parameters *) fun not_in_sort x S' S = - "Type variable " ^ x ^ "::" ^ Sorts.str_of_sort S' ^ " not in sort " ^ + "Variable " ^ x ^ "::" ^ Sorts.str_of_sort S' ^ " not of sort " ^ Sorts.str_of_sort S ^ "."; fun meet _ [] = ()