src/HOL/Tools/ATP/atp_proof_reconstruct.ML

     end
 
 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
 
     (* Equations of the form "x = ..." or "... = x" or similar are too specific
        to be useful. Quantified formulas are also filtered out. As for "True",

           (@{const less_eq(nat)} $ @{const zero_class.zero(nat)} $ _)) => NONE
       | @{const Trueprop} $ (@{const Not} $
           (@{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
 
 end;