# HG changeset patch
# User paulson
# Date 1532258981 -7200
# Node ID f4ac69fe45096108b9715bb6f35bc5da4a0d32f4
# Parent  9247996782c95aac58e7515e55b294dac41f99b4# Parent  22d10f94811ed2b29872b572a9883b49eddef1a3
merged

diff -r 22d10f94811e -r f4ac69fe4509 src/HOL/TPTP/TPTP_Parser_Test.thy
--- a/src/HOL/TPTP/TPTP_Parser_Test.thy	Sun Jul 22 13:29:24 2018 +0200
+++ b/src/HOL/TPTP/TPTP_Parser_Test.thy	Sun Jul 22 13:29:41 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