# HG changeset patch
# User blanchet
# Date 1324403990 -3600
# Node ID c99af5431dfe4a1b2a4e021eee35ebe5ee35bc20
# Parent  818ec0118683f348b23ac637340499f2749aff4e
one more SPASS identifier

diff -r 818ec0118683 -r c99af5431dfe src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Dec 20 18:59:46 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Dec 20 18:59:50 2011 +0100
@@ -644,9 +644,9 @@
    ensure that "HOL.eq" is correctly mapped to equality (not clear whether this
    is still necessary). *)
 val spass_reserved_nice_names =
-  ["forall", "exists", "le", "ls", "ge", "gs", "plus", "minus", "mult", "fract",
-   "equal", "true", "false", "or", "and", "not", "implies", "implied", "equiv",
-   "lr", "def"]
+  ["and", "def", "equal", "equiv", "exists", "false", "forall", "fract", "ge",
+   "gs", "id", "implied", "implies", "le", "lr", "ls", "minus", "mult", "not",
+   "or", "plus", "true"]
 val reserved_nice_names =
   [tptp_old_equal, "op", "eq"] @ spass_reserved_nice_names