1.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Nov 08 11:49:28 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Nov 08 12:13:44 2010 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  structure T = Z3_Proof_Tools
     1.5  structure L = Z3_Proof_Literals
     1.6  
     1.7 -fun z3_exn msg = raise SMT_Solver.SMT (SMT_Solver.Other_Failure
     1.8 +fun z3_exn msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure
     1.9    ("Z3 proof reconstruction: " ^ msg))
    1.10  
    1.11  
    1.12 @@ -66,11 +66,11 @@
    1.13  (** proof tools **)
    1.14  
    1.15  fun named ctxt name prover ct =
    1.16 -  let val _ = SMT_Solver.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
    1.17 +  let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
    1.18    in prover ct end
    1.19  
    1.20  fun NAMED ctxt name tac i st =
    1.21 -  let val _ = SMT_Solver.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
    1.22 +  let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
    1.23    in tac i st end
    1.24  
    1.25  fun pretty_goal ctxt thms t =
    1.26 @@ -90,7 +90,7 @@
    1.27      fun apply [] ct = error (try_apply_err ct)
    1.28        | apply (prover :: provers) ct =
    1.29            (case try prover ct of
    1.30 -            SOME thm => (SMT_Solver.trace_msg ctxt I "Z3: succeeded"; thm)
    1.31 +            SOME thm => (SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm)
    1.32            | NONE => apply provers ct)
    1.33  
    1.34    in apply o cons (named ctxt "schematic rules" (by_schematic_rule ctxt)) end
    1.35 @@ -732,9 +732,9 @@
    1.36  in
    1.37  fun trace_rule idx prove r ps ct (cxp as (ctxt, ptab)) =
    1.38    let
    1.39 -    val _ = SMT_Solver.trace_msg ctxt (header idx r o count_rules) ptab
    1.40 +    val _ = SMT_Config.trace_msg ctxt (header idx r o count_rules) ptab
    1.41      val result as (p, (ctxt', _)) = prove r ps ct cxp
    1.42 -    val _ = if not (Config.get ctxt' SMT_Solver.trace) then ()
    1.43 +    val _ = if not (Config.get ctxt' SMT_Config.trace) then ()
    1.44        else check ctxt' idx r ps ct p
    1.45    in result end
    1.46  end
    1.47 @@ -844,7 +844,7 @@
    1.48      val (idx, (ptab, vars, cx)) = P.parse ctxt typs terms output
    1.49      val assms' = prepare_assms cx unfolds assms
    1.50    in
    1.51 -    if Config.get cx SMT_Solver.filter_only
    1.52 +    if Config.get cx SMT_Config.filter_only_facts
    1.53      then ((filter_assms cx assms' ptab idx [], @{thm TrueI}), cx)
    1.54      else apfst (pair []) (prove cx assms' vars idx ptab)
    1.55    end