--- 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
--- 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;