diff -r a5bab59d580b -r 97ad1687cec7 src/HOL/ex/Meson_Test.thy
--- a/src/HOL/ex/Meson_Test.thy	Tue Jul 27 10:36:22 2021 +0200
+++ b/src/HOL/ex/Meson_Test.thy	Wed Jul 28 10:21:02 2021 +0200
@@ -26,8 +26,8 @@
   ML_prf \<open>
     val ctxt = \<^context>;
     val prem25 = Thm.assume \<^cprop>\<open>\<not> ?thesis\<close>;
-    val nnf25 = Meson.make_nnf {if_simps = true} ctxt prem25;
-    val xsko25 = Meson.skolemize {if_simps = true} ctxt nnf25;
+    val nnf25 = Meson.make_nnf Meson.simp_options_all_true ctxt prem25;
+    val xsko25 = Meson.skolemize Meson.simp_options_all_true ctxt nnf25;
 \<close>
   apply (tactic \<open>cut_tac xsko25 1 THEN REPEAT (eresolve_tac \<^context> [exE] 1)\<close>)
   ML_val \<open>
@@ -50,8 +50,8 @@
   ML_prf \<open>
     val ctxt = \<^context>;
     val prem26 = Thm.assume \<^cprop>\<open>\<not> ?thesis\<close>
-    val nnf26 = Meson.make_nnf {if_simps = true} ctxt prem26;
-    val xsko26 = Meson.skolemize {if_simps = true} ctxt nnf26;
+    val nnf26 = Meson.make_nnf Meson.simp_options_all_true ctxt prem26;
+    val xsko26 = Meson.skolemize Meson.simp_options_all_true ctxt nnf26;
 \<close>
   apply (tactic \<open>cut_tac xsko26 1 THEN REPEAT (eresolve_tac \<^context> [exE] 1)\<close>)
   ML_val \<open>
@@ -77,8 +77,8 @@
   ML_prf \<open>
     val ctxt = \<^context>;
     val prem43 = Thm.assume \<^cprop>\<open>\<not> ?thesis\<close>;
-    val nnf43 = Meson.make_nnf {if_simps = true} ctxt prem43;
-    val xsko43 = Meson.skolemize {if_simps = true} ctxt nnf43;
+    val nnf43 = Meson.make_nnf Meson.simp_options_all_true ctxt prem43;
+    val xsko43 = Meson.skolemize Meson.simp_options_all_true ctxt nnf43;
 \<close>
   apply (tactic \<open>cut_tac xsko43 1 THEN REPEAT (eresolve_tac \<^context> [exE] 1)\<close>)
   ML_val \<open>