1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 14:12:55 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 14:29:39 2011 +0200
     1.3 @@ -314,11 +314,16 @@
     1.4        tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
     1.5  fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
     1.6  
     1.7 -(* "HOL.eq" is mapped to the ATP's equality. *)
     1.8 -fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
     1.9 -  | make_fixed_const (SOME (THF With_Choice)) "Hilbert_Choice.Eps"(*FIXME*) =
    1.10 -      tptp_choice
    1.11 -  | make_fixed_const _ c = const_prefix ^ lookup_const c
    1.12 +(* "HOL.eq" and Choice are mapped to the ATP's equivalents *)
    1.13 +local
    1.14 +  val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
    1.15 +  fun default c = const_prefix ^ lookup_const c
    1.16 +in
    1.17 +  fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
    1.18 +    | make_fixed_const (SOME (THF With_Choice)) c =
    1.19 +        if c = choice_const then tptp_choice else default c
    1.20 +    | make_fixed_const _ c = default c
    1.21 +end
    1.22  
    1.23  fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
    1.24