--- 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