src/HOL/Tools/Meson/meson_tactic.ML
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