# HG changeset patch
# User nik
# Date 1314707379 -7200
# Node ID 0f50f158eb5741e5baa3c76928274cdbd4ccacb8
# Parent  eeba1eedf32d21ded409f161f23456aec7bd5c0d
removed explicit reliance on Hilbert_Choice.Eps

diff -r eeba1eedf32d -r 0f50f158eb57 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 14:12:55 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 14:29:39 2011 +0200
@@ -314,11 +314,16 @@
       tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
 
-(* "HOL.eq" is mapped to the ATP's equality. *)
-fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
-  | make_fixed_const (SOME (THF With_Choice)) "Hilbert_Choice.Eps"(*FIXME*) =
-      tptp_choice
-  | make_fixed_const _ c = const_prefix ^ lookup_const c
+(* "HOL.eq" and Choice are mapped to the ATP's equivalents *)
+local
+  val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
+  fun default c = const_prefix ^ lookup_const c
+in
+  fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
+    | make_fixed_const (SOME (THF With_Choice)) c =
+        if c = choice_const then tptp_choice else default c
+    | make_fixed_const _ c = default c
+end
 
 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c