avoid redundant argument (amending af6f55b15749);
authorwenzelm
Mon, 14 Jul 2025 12:23:32 +0200
changeset 82866 bfd8258133a1
parent 82865 639ceaf8eb0d
child 82867 75064081894e
avoid redundant argument (amending af6f55b15749);
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";