special treatment of extensionality in minimizer

--- a/src/HOL/Tools/ATP/atp_proof.ML	Sun Oct 12 21:52:45 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Sun Oct 12 21:52:45 2014 +0200
@@ -18,6 +18,7 @@
   exception UNRECOGNIZED_ATP_PROOF of unit
 
   datatype atp_failure =
+    MaybeUnprovable |
     Unprovable |
     GaveUp |
     ProofMissing |
@@ -145,6 +146,7 @@
 exception UNRECOGNIZED_ATP_PROOF of unit
 
 datatype atp_failure =
+  MaybeUnprovable |
   Unprovable |
   GaveUp |
   ProofMissing |
@@ -177,7 +179,8 @@
 fun from_lemmas [] = ""
   | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss))
 
-fun string_of_atp_failure Unprovable = "The generated problem is unprovable."
+fun string_of_atp_failure MaybeUnprovable = "The generated problem is maybe unprovable."
+  | string_of_atp_failure Unprovable = "The generated problem is unprovable."
   | string_of_atp_failure GaveUp = "The prover gave up."
   | string_of_atp_failure ProofMissing =
     "The prover claims the conjecture is a theorem but did not provide a proof."

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Sun Oct 12 21:52:45 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Sun Oct 12 21:52:45 2014 +0200
@@ -180,7 +180,8 @@
 fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
 
 fun filter_used_facts keep_chained used =
-  filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
+  filter ((member (eq_fst (op =)) used o fst) orf
+    (if keep_chained then is_fact_chained else K false))
 
 val max_fact_instances = 10 (* FUDGE *)
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Sun Oct 12 21:52:45 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Sun Oct 12 21:52:45 2014 +0200
@@ -99,7 +99,16 @@
     val problem =
       {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
        factss = [("", facts)]}
-    val result as {outcome, used_facts, run_time, ...} = prover params problem
+    val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time,
+        message} =
+      prover params problem
+    val result as {outcome, ...} =
+      if is_none outcome0 andalso
+         forall (member (fn ((s, _), ((s', _), _)) => s = s') used_from) used_facts then
+        result0
+      else
+        {outcome = SOME MaybeUnprovable, used_facts = [], used_from = used_from,
+         preferred_methss = preferred_methss, run_time = run_time, message = message}
   in
     print silent (fn () =>
       (case outcome of