author | blanchet |
Tue, 27 Mar 2012 16:59:13 +0300 | |
changeset 47146 | 7276f2b12ff7 |
parent 47145 | ffc6d6267a88 |
child 47147 | bd064bc71085 |
--- 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)))