# 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 *)