--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Feb 20 08:44:24 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Feb 20 08:44:24 2013 +0100
@@ -158,6 +158,10 @@
fun slack_fastype_of t = fastype_of t handle TERM _ => HOLogic.typeT
+(* Cope with "tt(X) = X" atoms, where "X" is existentially quantified. *)
+fun loose_aconv (Free (s, _), Free (s', _)) = s = s'
+ | loose_aconv (t, t') = t aconv t'
+
val vampire_skolem_prefix = "sK"
(* First-order translation. No types are known for variables. "HOLogic.typeT"
@@ -178,8 +182,7 @@
else if s = tptp_equal then
let val ts = map (do_term [] NONE) us in
if textual andalso length ts = 2 andalso
- hd ts aconv List.last ts then
- (* Vampire is keen on producing these. *)
+ loose_aconv (hd ts, List.last ts) then
@{const True}
else
list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Feb 20 08:44:24 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Feb 20 08:44:24 2013 +0100
@@ -395,8 +395,6 @@
line :: lines
(* Is there a repetition? If so, replace later line by earlier one. *)
else case take_prefix (not o is_same_inference (role, t)) lines of
- (* FIXME: Doesn't this code risk conflating proofs involving different
- types? *)
(_, []) => line :: lines
| (pre, Inference_Step (name', _, _, _, _) :: post) =>
line :: pre @ map (replace_dependencies_in_line (name', [name])) post