# HG changeset patch
# User blanchet
# Date 1370657842 14400
# Node ID dba3d398c3226462037c8ea9c9529598b54385f8
# Parent  891e128ea08cf5f53de9f676144d970df5c629e0
SPASS has more Uppercase keywords than I was fearing -- better always append _

diff -r 891e128ea08c -r dba3d398c322 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Fri Jun 07 22:17:19 2013 -0400
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Fri Jun 07 22:17:22 2013 -0400
@@ -899,8 +899,7 @@
        String.isSubstring "_" s then
       s
     else if is_tptp_variable s then
-      (* "DL" appears to be a SPASS 3.7 keyword *)
-      if s = "DL" then s ^ "_" else s
+      s ^ "_"
     else
       String.substring (s, 0, n - 1) ^
       String.str (Char.toUpper (String.sub (s, n - 1)))