diff -r fcd118d9242f -r 24b17460ee60 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Fri Aug 19 05:49:09 2022 +0000
+++ b/src/HOL/Tools/lin_arith.ML	Fri Aug 19 05:49:10 2022 +0000
@@ -104,6 +104,15 @@
 val neq_limit = Attrib.setup_config_int \<^binding>\<open>linarith_neq_limit\<close> (K 9);
 val trace = Attrib.setup_config_bool \<^binding>\<open>linarith_trace\<close> (K false);
 
+fun nnf_simpset ctxt =
+  (empty_simpset ctxt
+    |> Simplifier.set_mkeqTrue mk_eq_True
+    |> Simplifier.set_mksimps (mksimps mksimps_pairs))
+  addsimps @{thms imp_conv_disj iff_conv_conj_imp de_Morgan_disj
+    de_Morgan_conj not_all not_ex not_not}
+
+fun prem_nnf_tac ctxt = full_simp_tac (nnf_simpset ctxt)
+
 
 structure LA_Data: LIN_ARITH_DATA =
 struct
@@ -764,6 +773,7 @@
     result
   end;
 
+
 (* takes the i-th subgoal  [| A1; ...; An |] ==> B  to                       *)
 (* An --> ... --> A1 --> B,  performs splitting with the given 'split_thms'  *)
 (* (resulting in a different subgoal P), takes  P  to  ~P ==> False,         *)
@@ -773,16 +783,6 @@
 (* general form  [| Q1; ...; Qm |] ==> False.  Fails if more than            *)
 (* !split_limit splits are possible.                              *)
 
-local
-  fun nnf_simpset ctxt =
-    (empty_simpset ctxt
-      |> Simplifier.set_mkeqTrue mk_eq_True
-      |> Simplifier.set_mksimps (mksimps mksimps_pairs))
-    addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
-      @{thm de_Morgan_conj}, not_all, not_ex, not_not]
-  fun prem_nnf_tac ctxt = full_simp_tac (nnf_simpset ctxt)
-in
-
 fun split_once_tac ctxt split_thms =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -813,8 +813,6 @@
     ]
   end;
 
-end;  (* local *)
-
 (* remove irrelevant premises, then split the i-th subgoal (and all new      *)
 (* subgoals) by using 'split_once_tac' repeatedly.  Beta-eta-normalize new   *)
 (* subgoals and finally attempt to solve them by finding an immediate        *)
@@ -897,16 +895,6 @@
    where the Ai are atomic, i.e. no top-level &, | or EX
 *)
 
-local
-  fun nnf_simpset ctxt =
-    (empty_simpset ctxt
-      |> Simplifier.set_mkeqTrue mk_eq_True
-      |> Simplifier.set_mksimps (mksimps mksimps_pairs))
-    addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
-      @{thm de_Morgan_conj}, @{thm not_all}, @{thm not_ex}, @{thm not_not}];
-  fun prem_nnf_tac ctxt = full_simp_tac (nnf_simpset ctxt);
-in
-
 fun refute_tac ctxt test prep_tac ref_tac =
   let val refute_prems_tac =
         REPEAT_DETERM
@@ -921,8 +909,6 @@
             SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
   end;
 
-end;
-
 
 (* arith proof method *)