changeset 81254 | d3c0734059ee |
parent 75009 | d2f97439f53e |
--- a/src/HOL/Tools/Meson/meson_tactic.ML Thu Oct 24 22:05:57 2024 +0200 +++ b/src/HOL/Tools/Meson/meson_tactic.ML Fri Oct 25 15:31:58 2024 +0200 @@ -17,7 +17,7 @@ let val ctxt' = put_claset HOL_cs ctxt in Meson.meson_tac ctxt' (maps (snd o Meson_Clausify.cnf_axiom Meson.simp_options_all_true ctxt' - false true 0) ths) + {new_skolem = false, combs = true, refl = true} 0) ths) end (* This is part of a workaround to avoid freezing schematic variables in \<^text>\<open>using\<close> facts. See