--- a/src/Pure/POLY.ML Wed Mar 05 10:02:53 1997 +0100 +++ b/src/Pure/POLY.ML Wed Mar 05 10:03:30 1997 +0100 @@ -123,5 +123,5 @@ end; - +(*Non-printing and 8-bit chars are forbidden in string constants*) val needs_filtered_use = true;