1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Mar 27 16:59:13 2012 +0300
1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Mar 27 16:59:13 2012 +0300
1.3 @@ -785,6 +785,9 @@
1.4 if n < 2 orelse (n = 2 andalso String.sub (s, 0) = String.sub (s, 1)) orelse
1.5 String.isSubstring "_" s then
1.6 s
1.7 + else if s = "Dl" orelse s = "DL" then
1.8 + (* "DL" appears to be a SPASS 3.7 keyword *)
1.9 + s ^ "_"
1.10 else
1.11 String.substring (s, 0, n - 1) ^
1.12 String.str (Char.toUpper (String.sub (s, n - 1)))