1.1 --- a/src/HOL/SMT/Tools/z3_proof_rules.ML	Fri Nov 13 15:47:37 2009 +0100
     1.2 +++ b/src/HOL/SMT/Tools/z3_proof_rules.ML	Wed Nov 18 14:00:08 2009 +0100
     1.3 @@ -18,6 +18,7 @@
     1.4      thm
     1.5  
     1.6    (*setup*)
     1.7 +  val trace_assms: bool Config.T
     1.8    val setup: theory -> theory
     1.9  end
    1.10  
    1.11 @@ -474,6 +475,9 @@
    1.12  
    1.13  val true_false = @{lemma "True == ~ False" by simp}
    1.14  
    1.15 +val (trace_assms, trace_assms_setup) =
    1.16 +  Attrib.config_bool "z3_trace_assms" false
    1.17 +
    1.18  local
    1.19    val TT_eq = @{lemma "(P = (~False)) == P" by simp}
    1.20    val remove_trigger = @{lemma "trigger t p == p"
    1.21 @@ -491,10 +495,15 @@
    1.22  
    1.23    val threshold = 10
    1.24    
    1.25 +  fun trace ctxt thm =
    1.26 +    if Config.get ctxt trace_assms
    1.27 +    then tracing (Display.string_of_thm ctxt thm)
    1.28 +    else ()
    1.29 +
    1.30    val lookup = (fn Some thms => first_of thms | Many net => net_instance net)
    1.31    fun lookup_assm ctxt assms ct =
    1.32      (case lookup assms ct of
    1.33 -      SOME thm => thm
    1.34 +      SOME thm => (trace ctxt thm; thm)
    1.35      | _ => z3_exn ("not asserted: " ^
    1.36          quote (Syntax.string_of_term ctxt (Thm.term_of ct))))
    1.37  in
    1.38 @@ -1392,6 +1401,6 @@
    1.39  
    1.40    in (fn ptab => fn idx => result (fst (lookup idx ptab))) end
    1.41  
    1.42 -val setup = Z3_Rewrite_Rules.setup
    1.43 +val setup = trace_assms_setup #> Z3_Rewrite_Rules.setup
    1.44  
    1.45  end