# HG changeset patch
# User blanchet
# Date 1332856753 -10800
# Node ID 7276f2b12ff7f4f413147c0c49cc582c374a3037
# Parent  ffc6d6267a880bd956e61531c006c6db397e24f4
avoid DL

diff -r ffc6d6267a88 -r 7276f2b12ff7 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Mar 27 16:59:13 2012 +0300
@@ -785,6 +785,9 @@
     if n < 2 orelse (n = 2 andalso String.sub (s, 0) = String.sub (s, 1)) orelse
        String.isSubstring "_" s then
       s
+    else if s = "Dl" orelse s = "DL" then
+      (* "DL" appears to be a SPASS 3.7 keyword *)
+      s ^ "_"
     else
       String.substring (s, 0, n - 1) ^
       String.str (Char.toUpper (String.sub (s, n - 1)))