# HG changeset patch # User wenzelm # Date 1752488612 -7200 # Node ID bfd8258133a1435c7dde6ab554bf5f567bdb4069 # Parent 639ceaf8eb0d53d7e9e0c509a7bf44eafcb20682 avoid redundant argument (amending af6f55b15749); diff -r 639ceaf8eb0d -r bfd8258133a1 src/Provers/classical.ML --- a/src/Provers/classical.ML Mon Jul 14 11:46:14 2025 +0200 +++ b/src/Provers/classical.ML Mon Jul 14 12:23:32 2025 +0200 @@ -364,7 +364,7 @@ let val _ = Thm.no_prems th andalso err_thm_illformed ctxt kind th; val th' = classical_rule ctxt (flat_rule ctxt th); - val dup_th' = dup_elim ctxt th' handle THM _ => err_thm_illformed ctxt kind th th; + val dup_th' = dup_elim ctxt th' handle THM _ => err_thm_illformed ctxt kind th; in make_info (no_swapped_rl th') (no_swapped_rl dup_th') th end else raise Fail "Bad rule kind";