--- a/src/HOL/Tools/Meson/meson.ML Thu Oct 24 22:05:57 2024 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Fri Oct 25 15:31:58 2024 +0200
@@ -16,7 +16,7 @@
val size_of_subgoals: thm -> int
val has_too_many_clauses: Proof.context -> term -> bool
val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
- val finish_cnf: thm list -> thm list
+ val finish_cnf: bool -> thm list -> thm list
val presimplified_consts : string list
val presimplify: simp_options -> Proof.context -> thm -> thm
val make_nnf: simp_options -> Proof.context -> thm -> thm
@@ -277,7 +277,7 @@
(*Simplify a clause by applying reflexivity to its negated equality literals*)
fun refl_clause th =
let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (Thm.concl_of th))
- in zero_var_indexes (refl_clause_aux neqs th) end
+ in refl_clause_aux neqs th end
handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*)
@@ -408,8 +408,11 @@
fun make_cnf old_skolem_ths th ctxt =
cnf old_skolem_ths ctxt (th, [])
-(*Generalization, removal of redundant equalities, removal of tautologies.*)
-fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);
+(*Generalization, optional removal of redundant equalities, removal of tautologies.*)
+fun finish_cnf refl ths = ths
+ |> refl ? map refl_clause
+ |> map zero_var_indexes
+ |> filter (not o is_taut)
(**** Generation of contrapositives ****)