# HG changeset patch
# User blanchet
# Date 1283460596 -7200
# Node ID ceee95f4182338b1552c0a9b5ea389efc9ad144e
# Parent  d08fdb351345448c125785112a4bbd73d93b5bab
fix bug in "debug" mode

diff -r d08fdb351345 -r ceee95f41823 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Sep 02 22:15:20 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Sep 02 22:49:56 2010 +0200
@@ -111,9 +111,10 @@
 fun pool_map f xs =
   pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
 
-(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the
-   unreadable "op_1", "op_2", etc., in the problem files. *)
-val reserved_nice_names = ["equal", "op"]
+(* "op" is also reserved, to avoid the unreadable "op_1", "op_2", etc., in the
+   problem files. "equal" is reserved by some ATPs. "eq" is reserved to ensure
+   that "HOL.eq" is correctly mapped to equality. *)
+val reserved_nice_names = ["op", "equal", "eq"]
 fun readable_name full_name s =
   if s = full_name then
     s