diff -r 205749fba102 -r 9247996782c9 src/HOL/TPTP/TPTP_Parser_Test.thy
--- a/src/HOL/TPTP/TPTP_Parser_Test.thy	Sat Jul 21 23:25:22 2018 +0200
+++ b/src/HOL/TPTP/TPTP_Parser_Test.thy	Sun Jul 22 13:00:38 2018 +0200
@@ -30,14 +30,14 @@
         Nonstandard "OTH123.p"),
      ("other",
         Nonstandard "other"),
-     ("AAA000£0.axiom",
-        Nonstandard "AAA000£0.axiom"),
-     ("AAA000£0.p",
-        Nonstandard "AAA000£0.p"),
+     ("AAA000\194\1630.axiom",
+        Nonstandard "AAA000\194\1630.axiom"),
+     ("AAA000\194\1630.p",
+        Nonstandard "AAA000\194\1630.p"),
      ("AAA000.0.p",
         Nonstandard "AAA000.0.p"),
-     ("AAA000£0.what",
-        Nonstandard "AAA000£0.what"),
+     ("AAA000\194\1630.what",
+        Nonstandard "AAA000\194\1630.what"),
      ("",
         Nonstandard "")];
 in