# HG changeset patch
# User blanchet
# Date 1678294316 -3600
# Node ID 80bcebe6cf33b0497e2d0c13a149e58e4bfdc820
# Parent  72a99b54e2067129158dcee00a6e66d6186d440b
require the presence of free variables to do abduction in Sledgehammer

diff -r 72a99b54e206 -r 80bcebe6cf33 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Mar 08 10:12:41 2023 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Mar 08 17:51:56 2023 +0100
@@ -824,7 +824,7 @@
 fun top_abduce_candidates max_candidates candidates =
   let
     (* We prefer free variables to other constructs, so that e.g. "x \<le> y" is
-       prioritized over "x \<le> 0". *)
+       prioritized over "x \<le> 5". *)
     fun score t =
       Term.fold_aterms (fn t => fn score => score + (case t of Free _ => 1 | _ => 2)) t 0
 
@@ -849,7 +849,12 @@
           (@{const less_eq(nat)} $ @{const one_class.one(nat)} $ _)) => NONE
       | @{const Trueprop} $ (Const (@{const_name All}, _) $ _) => NONE
       | @{const Trueprop} $ (Const (@{const_name Ex}, _) $ _) => NONE
-      | _ => SOME (score t, t))
+      | _ =>
+        (* We require the presence of at least one free variable. A "missing
+           assumption" that does not talk about any free variable is likely
+           spurious. *)
+        if exists_subterm (fn Free _ => true | _ => false) t then SOME (score t, t)
+        else NONE)
   in
     sort_top max_candidates (map_filter maybe_score candidates)
   end