--- a/src/HOL/Tools/Metis/metis_translate.ML Tue Jun 07 08:58:23 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Tue Jun 07 10:43:18 2011 +0200
@@ -20,6 +20,10 @@
val metis_app_op : string
val metis_type_tag : string
val metis_generated_var_prefix : string
+ val trace : bool Config.T
+ val verbose : bool Config.T
+ val trace_msg : Proof.context -> (unit -> string) -> unit
+ val verbose_warning : Proof.context -> string -> unit
val metis_name_table : ((string * int) * (string * bool)) list
val reveal_old_skolem_terms : (string * term) list -> term -> term
val prepare_metis_problem :
@@ -39,6 +43,13 @@
val metis_type_tag = ":"
val metis_generated_var_prefix = "_"
+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 =
+ if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
+
val metis_name_table =
[((tptp_equal, 2), (metis_equal, false)),
((tptp_old_equal, 2), (metis_equal, false)),
@@ -163,7 +174,8 @@
I
else
map (pair 0)
- #> rpair ctxt
+ #> rpair (ctxt |> not (Config.get ctxt verbose)
+ ? Config.put Monomorph.verbose false)
#-> Monomorph.monomorph Monomorph.all_schematic_consts_of
#> fst #> maps (map (zero_var_indexes o snd)))
val (old_skolems, props) =