--- 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