# HG changeset patch
# User wenzelm
# Date 1414587440 -3600
# Node ID 4cd778c91fdcb541066473b8e01d5d6f28d60ce9
# Parent  aab139c0003fc8248c3c55feb7e849cc4747b4ae
modernized setup;

diff -r aab139c0003f -r 4cd778c91fdc src/HOL/Meson.thy
--- a/src/HOL/Meson.thy	Wed Oct 29 13:42:38 2014 +0100
+++ b/src/HOL/Meson.thy	Wed Oct 29 13:57:20 2014 +0100
@@ -195,8 +195,6 @@
 ML_file "Tools/Meson/meson_clausify.ML"
 ML_file "Tools/Meson/meson_tactic.ML"
 
-setup {* Meson_Tactic.setup *}
-
 hide_const (open) COMBI COMBK COMBB COMBC COMBS skolem
 hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD
     not_impD iff_to_disjD not_iffD not_refl_disj_D conj_exD1 conj_exD2 disj_exD
diff -r aab139c0003f -r 4cd778c91fdc src/HOL/Tools/Meson/meson_tactic.ML
--- a/src/HOL/Tools/Meson/meson_tactic.ML	Wed Oct 29 13:42:38 2014 +0100
+++ b/src/HOL/Tools/Meson/meson_tactic.ML	Wed Oct 29 13:57:20 2014 +0100
@@ -8,21 +8,19 @@
 signature MESON_TACTIC =
 sig
   val meson_general_tac : Proof.context -> thm list -> int -> tactic
-  val setup: theory -> theory
 end;
 
 structure Meson_Tactic : MESON_TACTIC =
 struct
 
-open Meson_Clausify
-
 fun meson_general_tac ctxt ths =
   let val ctxt' = put_claset HOL_cs ctxt
-  in Meson.meson_tac ctxt' (maps (snd o cnf_axiom ctxt' false true 0) ths) end
+  in Meson.meson_tac ctxt' (maps (snd o Meson_Clausify.cnf_axiom ctxt' false true 0) ths) end
 
-val setup =
-  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
-     SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
-     "MESON resolution proof procedure"
+val _ =
+  Theory.setup
+    (Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
+      SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
+      "MESON resolution proof procedure")
 
 end;