src/Pure/POLY.ML

      close_in is;
      result
   end;
 
 
-
+(*Non-printing and 8-bit chars are forbidden in string constants*)
 val needs_filtered_use = true;