# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1729867095 -7200
# Node ID 2f11cd18aa96575b00cdae7e6218686c0b75a836
# Parent  daf5697035b5ecc4c2a5eed8d81ab4ca53f397df
try0: filter out untagged thms;

diff -r daf5697035b5 -r 2f11cd18aa96 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Thu Oct 24 19:13:49 2024 +0200
+++ b/src/HOL/Tools/try0.ML	Fri Oct 25 16:38:15 2024 +0200
@@ -10,7 +10,7 @@
   val silence_methods : bool -> Proof.context -> Proof.context
   datatype modifier = Use | Simp | Intro | Elim | Dest
   type result = {name: string, command: string, time: int, state: Proof.state}
-  val try0 : Time.time option -> ((Facts.ref * Token.src list)  * modifier list) list -> 
+  val try0 : Time.time option -> ((Facts.ref * Token.src list)  * modifier list) list ->
     Proof.state -> result list
 end
 
@@ -64,7 +64,11 @@
   if mode <> Auto_Try orelse run_if_auto_try then
     let
       val unused =
-        tagged |> filter (fn (_, tags) => null (inter (op =) tags (attrs |> map fst))) |> map fst
+        tagged
+        |> filter
+          (fn (_, tags) => not (null tags) andalso null (inter (op =) tags (attrs |> map fst)))
+        |> map fst
+
       val attrs = attrs_text attrs tagged
 
       val ctxt = Proof.context_of st