--- a/src/HOL/Tools/ATP/atp_problem.ML Thu Feb 02 01:20:28 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Feb 02 01:55:17 2012 +0100
@@ -49,7 +49,7 @@
val introN : string
val elimN : string
val simpN : string
- val eqN : string
+ val spec_eqN : string
val tptp_cnf : string
val tptp_fof : string
val tptp_tff : string
@@ -169,7 +169,7 @@
val introN = "intro"
val elimN = "elim"
val simpN = "simp"
-val eqN = "eq"
+val spec_eqN = "spec_eq"
fun extract_isabelle_info (SOME (ATerm ("[]", [ATerm (s, [])]))) =
try (unprefix isabelle_info_prefix) s
@@ -441,7 +441,7 @@
if top_level then
case extract_isabelle_info info of
SOME s' => if s' = simpN then s ^ ":lr"
- else if s' = eqN then s ^ ":lt"
+ else if s' = spec_eqN then s ^ ":lt"
else s
| NONE => s
else