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 @@ -125,7 +125,7 @@
     1.4      (string * string) problem -> (string * string) problem
     1.5    val filter_cnf_ueq_problem :
     1.6      (string * string) problem -> (string * string) problem
     1.7 -  val declared_syms_in_problem : (string * ''a) problem -> (string * ''a) list
     1.8 +  val declared_syms_in_problem : 'a problem -> 'a list
     1.9    val nice_atp_problem :
    1.10      bool -> atp_format -> ('a * (string * string) problem_line list) list
    1.11      -> ('a * string problem_line list) list
    1.12 @@ -689,7 +689,7 @@
    1.13  
    1.14  (** Symbol declarations **)
    1.15  
    1.16 -fun add_declared_syms_in_problem_line (Decl (_, sym, _)) = insert (op =) sym
    1.17 +fun add_declared_syms_in_problem_line (Decl (_, sym, _)) = cons sym
    1.18    | add_declared_syms_in_problem_line _ = I
    1.19  fun declared_syms_in_problem problem =
    1.20    fold (fold add_declared_syms_in_problem_line o snd) problem []
    1.21 @@ -785,9 +785,9 @@
    1.22      if n < 2 orelse (n = 2 andalso String.sub (s, 0) = String.sub (s, 1)) orelse
    1.23         String.isSubstring "_" s then
    1.24        s
    1.25 -    else if s = "Dl" orelse s = "DL" then
    1.26 +    else if is_tptp_variable s then
    1.27        (* "DL" appears to be a SPASS 3.7 keyword *)
    1.28 -      s ^ "_"
    1.29 +      if s = "DL" then s ^ "_" else s
    1.30      else
    1.31        String.substring (s, 0, n - 1) ^
    1.32        String.str (Char.toUpper (String.sub (s, n - 1)))