src/HOL/Tools/Metis/metis_reconstruct.ML

 sig
   type mode = Metis_Translate.mode
 
   val trace : bool Config.T
   val trace_msg : Proof.context -> (unit -> string) -> unit
+  val verbose : bool Config.T
+  val verbose_warning : Proof.context -> string -> unit
   val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
   val untyped_aconv : term -> term -> bool
   val replay_one_inference :
     Proof.context -> mode -> (string * term) list * int Unsynchronized.ref
     -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list

 struct
 
 open Metis_Translate
 
 val (trace, trace_setup) = Attrib.config_bool "trace_metis" (K false)
+val (verbose, verbose_setup) = Attrib.config_bool "verbose_metis" (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 msg else ()
 
 datatype term_or_type = SomeTerm of term | SomeType of typ
 
 fun terms_of [] = []
   | terms_of (SomeTerm t :: tts) = t :: terms_of tts

       handle ERROR _ =>
              error ("Cannot replay Metis proof in Isabelle:\n\
                     \Error when discharging Skolem assumptions.")
     end
 
-val setup = trace_setup
+val setup = trace_setup #> verbose_setup
 
 end;