avoid DL
authorblanchet
Tue, 27 Mar 2012 16:59:13 +0300
changeset 480177276f2b12ff7
parent 48016 ffc6d6267a88
child 48018 bd064bc71085
avoid DL
src/HOL/Tools/ATP/atp_problem.ML
     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)))