src/HOL/SMT/Tools/z3_proof_rules.ML

   val make_proof: rule -> int list -> cterm * cterm list -> proof
   val prove: Proof.context -> thm list option -> proof Inttab.table -> int ->
     thm
 
   (*setup*)
+  val trace_assms: bool Config.T
   val setup: theory -> theory
 end
 
 structure Z3_Proof_Rules: Z3_PROOF_RULES =
 struct

 
 datatype assms = Some of thm list | Many of thm Net.net
 
 val true_false = @{lemma "True == ~ False" by simp}
 
+val (trace_assms, trace_assms_setup) =
+  Attrib.config_bool "z3_trace_assms" false
+
 local
   val TT_eq = @{lemma "(P = (~False)) == P" by simp}
   val remove_trigger = @{lemma "trigger t p == p"
     by (rule eq_reflection, rule trigger_def)}
   val remove_iff = @{lemma "p iff q == p = q"

   val TT_eq_conv = Conv.rewr_conv TT_eq
   val norm_conv = More_Conv.bottom_conv (K (Conv.try_conv TT_eq_conv))
 
   val threshold = 10
   
+  fun trace ctxt thm =
+    if Config.get ctxt trace_assms
+    then tracing (Display.string_of_thm ctxt thm)
+    else ()
+
   val lookup = (fn Some thms => first_of thms | Many net => net_instance net)
   fun lookup_assm ctxt assms ct =
     (case lookup assms ct of
-      SOME thm => thm
+      SOME thm => (trace ctxt thm; thm)
     | _ => z3_exn ("not asserted: " ^
         quote (Syntax.string_of_term ctxt (Thm.term_of ct))))
 in
 fun prepare_assms ctxt assms =
   let

     fun result (hyps, (thm, _)) =
       fold SMT_Normalize.discharge_definition hyps (thm_of thm)
 
   in (fn ptab => fn idx => result (fst (lookup idx ptab))) end
 
-val setup = Z3_Rewrite_Rules.setup
-
-end
+val setup = trace_assms_setup #> Z3_Rewrite_Rules.setup
+
+end