# HG changeset patch
# User blanchet
# Date 1644400054 -3600
# Node ID 7cadf5a7ed5bc9165322e8df069739d571a9ec78
# Parent  41fd2e8f6b16a00c464e2268541062345f8a00a0
more liberal parsing of Sledgehammer options to allow empty lists (as suggested by Larry Paulson)

diff -r 41fd2e8f6b16 -r 7cadf5a7ed5b src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Feb 07 16:59:37 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Feb 09 10:47:34 2022 +0100
@@ -343,7 +343,9 @@
 val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm)
 val parse_fact_override_chunk =
   (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override)
+  || (Args.add |-- Args.colon |-- Scan.succeed [] >> add_fact_override)
   || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override)
+  || (Args.del |-- Args.colon |-- Scan.succeed [] >> del_fact_override)
   || (parse_fact_refs >> only_fact_override)
 val parse_fact_override =
   Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk >> merge_fact_overrides))