# HG changeset patch
# User wenzelm
# Date 1565601370 -7200
# Node ID 06a62b29085e041171c424ac1f7a0af2628e7981
# Parent  3f5d7fbaa1ea6171226f19a358de262d69199fca
do not open ML structures;

diff -r 3f5d7fbaa1ea -r 06a62b29085e src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Mon Aug 12 11:15:57 2019 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Mon Aug 12 11:16:10 2019 +0200
@@ -23,8 +23,6 @@
 structure Meson_Clausify : MESON_CLAUSIFY =
 struct
 
-open Meson
-
 (* the extra "Meson" helps prevent clashes (FIXME) *)
 val new_skolem_var_prefix = "MesonSK"
 val new_nonskolem_var_prefix = "MesonV"
@@ -306,14 +304,14 @@
          |> new_skolem ? forall_intr_vars
     val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
     val th = th |> Conv.fconv_rule (Object_Logic.atomize ctxt)
-                |> cong_extensionalize_thm ctxt
-                |> abs_extensionalize_thm ctxt
-                |> make_nnf ctxt
+                |> Meson.cong_extensionalize_thm ctxt
+                |> Meson.abs_extensionalize_thm ctxt
+                |> Meson.make_nnf ctxt
   in
     if new_skolem then
       let
         fun skolemize choice_ths =
-          skolemize_with_choice_theorems ctxt choice_ths
+          Meson.skolemize_with_choice_theorems ctxt choice_ths
           #> simplify (ss_only @{thms all_simps[symmetric]} ctxt)
         val no_choice = null choice_ths
         val pull_out =
@@ -323,7 +321,7 @@
             skolemize choice_ths
         val discharger_th = th |> pull_out
         val discharger_th =
-          discharger_th |> has_too_many_clauses ctxt (Thm.concl_of discharger_th)
+          discharger_th |> Meson.has_too_many_clauses ctxt (Thm.concl_of discharger_th)
                            ? (to_definitional_cnf_with_quantifiers ctxt
                               #> pull_out)
         val zapped_th =
@@ -356,18 +354,18 @@
          (NONE, (th, ctxt))
       end
     else
-      (NONE, (th |> has_too_many_clauses ctxt (Thm.concl_of th)
+      (NONE, (th |> Meson.has_too_many_clauses ctxt (Thm.concl_of th)
                     ? to_definitional_cnf_with_quantifiers ctxt, ctxt))
   end
 
 (* Convert a theorem to CNF, with additional premises due to skolemization. *)
 fun cnf_axiom ctxt0 new_skolem combinators ax_no th =
   let
-    val choice_ths = choice_theorems (Proof_Context.theory_of ctxt0)
+    val choice_ths = Meson.choice_theorems (Proof_Context.theory_of ctxt0)
     val (opt, (nnf_th, ctxt1)) =
       nnf_axiom choice_ths new_skolem ax_no th ctxt0
     fun clausify th =
-      make_cnf
+      Meson.make_cnf
        (if new_skolem orelse null choice_ths then []
         else map (old_skolem_theorem_of_def ctxt1) (old_skolem_defs th))
        th ctxt1
@@ -383,7 +381,7 @@
      cnf_ths |> map (combinators ? introduce_combinators_in_theorem ctxt2
                      #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
              |> Variable.export ctxt2 ctxt0
-             |> finish_cnf
+             |> Meson.finish_cnf
              |> map (Thm.close_derivation \<^here>))
   end
   handle THM _ => (NONE, [])