changeset 75002 | ef18787842b3 |
parent 74976 | 70aab133dc8d |
child 77269 | bc43f86c9598 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Jan 22 08:46:37 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Jan 22 11:33:31 2022 +0100 @@ -531,8 +531,7 @@ ||> op @ |> op @ end -fun nearly_all_facts ctxt inst_inducts {add, del, only} keywords css chained hyp_ts - concl_t = +fun nearly_all_facts ctxt inst_inducts {add, del, only} keywords css chained hyp_ts concl_t = if only andalso null add then [] else