# HG changeset patch
# User blanchet
# Date 1283457768 -7200
# Node ID 5ab6a37074990f80bd4e721e05b07ea7163d58f1
# Parent  c51e80de9b7e9d9f3f59aa83f34881b92055c70e
fix trivial "x = x" fact detection

diff -r c51e80de9b7e -r 5ab6a3707499 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Sep 02 15:48:32 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Sep 02 22:02:48 2010 +0200
@@ -315,8 +315,13 @@
           | _ => raise FO_TERM us
         else case strip_prefix_and_unascii const_prefix a of
           SOME "equal" =>
-          list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT),
-                     map (aux NONE []) us)
+          let val ts = map (aux NONE []) us in
+            if length ts = 2 andalso hd ts aconv List.last ts then
+              (* Vampire is keen on producing these. *)
+              @{const True}
+            else
+              list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
+          end
         | SOME b =>
           let
             val c = invert_const b
@@ -526,11 +531,6 @@
 fun is_bad_free frees (Free x) = not (member (op =) frees x)
   | is_bad_free _ _ = false
 
-(* Vampire is keen on producing these. *)
-fun is_trivial_formula (@{const Not} $ (Const (@{const_name HOL.eq}, _)
-                                        $ t1 $ t2)) = (t1 aconv t2)
-  | is_trivial_formula _ = false
-
 fun add_desired_line _ _ _ _ (line as Definition (num, _, _)) (j, lines) =
     (j, line :: map (replace_deps_in_line (num, [])) lines)
   | add_desired_line isar_shrink_factor conjecture_shape axiom_names frees
@@ -541,7 +541,6 @@
         (not (is_only_type_information t) andalso
          null (Term.add_tvars t []) andalso
          not (exists_subterm (is_bad_free frees) t) andalso
-         not (is_trivial_formula t) andalso
          (null lines orelse (* last line must be kept *)
           (length deps >= 2 andalso j mod isar_shrink_factor = 0))) then
        Inference (num, t, deps) :: lines  (* keep line *)