# HG changeset patch
# User blanchet
# Date 1361346264 -3600
# Node ID 4dc6bb65c3c3fb25c0a92ac6fe11d5404849e0ea
# Parent  89e9e945a005f426083192de0fd50a6f9dda5b4f
slacker comparison for Skolems, to avoid trivial equations

diff -r 89e9e945a005 -r 4dc6bb65c3c3 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- 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)
diff -r 89e9e945a005 -r 4dc6bb65c3c3 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- 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