# HG changeset patch
# User blanchet
# Date 1352728002 -3600
# Node ID fea589c8583e5a870c702553b152c727cc0fe78a
# Parent  c8d141cce517fc0ffc7221c09b0ef6b7d02352ca
fixed detection of tautologies -- things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies

diff -r c8d141cce517 -r fea589c8583e src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Nov 12 14:11:51 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Nov 12 14:46:42 2012 +0100
@@ -207,9 +207,12 @@
 
 fun is_likely_tautology_or_too_meta th =
   let
-    val is_boring_const = member (op =) atp_widely_irrelevant_consts
+    fun is_interesting_subterm (Const (s, _)) =
+        not (member (op =) atp_widely_irrelevant_consts s)
+      | is_interesting_subterm (Free _) = true
+      | is_interesting_subterm _ = false
     fun is_boring_bool t =
-      not (exists_Const (not o is_boring_const o fst) t) orelse
+      not (exists_subterm is_interesting_subterm t) orelse
       exists_type (exists_subtype (curry (op =) @{typ prop})) t
     fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t
       | is_boring_prop (@{const "==>"} $ t $ u) =
diff -r c8d141cce517 -r fea589c8583e src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Mon Nov 12 14:11:51 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Mon Nov 12 14:46:42 2012 +0100
@@ -536,8 +536,7 @@
   end
 
 (* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
-fun weight_of_fact rank =
-  Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
+fun weight_of_fact rank = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
 
 fun weight_mepo_facts facts =
   facts ~~ map weight_of_fact (0 upto length facts - 1)