SPASS has more Uppercase keywords than I was fearing -- better always append _
authorblanchet
Fri, 07 Jun 2013 22:17:22 -0400
changeset 52353 dba3d398c322
parent 52352 891e128ea08c
child 52354 acb4f932dd24
SPASS has more Uppercase keywords than I was fearing -- better always append _
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)))