--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon May 02 16:33:21 2011 +0200
@@ -23,7 +23,6 @@
-> (Metis_Thm.thm * thm) list
val discharge_skolem_premises :
Proof.context -> (thm * term) option list -> thm -> thm
- val setup : theory -> theory
end;
structure Metis_Reconstruct : METIS_RECONSTRUCT =
@@ -31,8 +30,8 @@
open Metis_Translate
-val (trace, trace_setup) = Attrib.config_bool "metis_trace" (K false)
-val (verbose, verbose_setup) = Attrib.config_bool "metis_verbose" (K true)
+val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
+val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
fun verbose_warning ctxt msg =
@@ -897,6 +896,4 @@
\Error when discharging Skolem assumptions.")
end
-val setup = trace_setup #> verbose_setup
-
end;