1.1 --- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Sun Jun 03 15:49:55 2012 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon Jun 04 09:07:23 2012 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4      Z3_Non_Commercial_Accepted |
     1.5      Z3_Non_Commercial_Declined
     1.6    val z3_non_commercial: unit -> z3_non_commercial
     1.7 +  val z3_with_extensions: bool Config.T
     1.8    val setup: theory -> theory
     1.9  end
    1.10  
    1.11 @@ -133,6 +134,9 @@
    1.12  end
    1.13  
    1.14  
    1.15 +val z3_with_extensions =
    1.16 +  Attrib.setup_config_bool @{binding z3_with_extensions} (K false)
    1.17 +
    1.18  local
    1.19    fun z3_make_command is_remote name () =
    1.20      if_z3_non_commercial (make_command is_remote name)
    1.21 @@ -163,11 +167,8 @@
    1.22        handle SMT_Failure.SMT _ => outcome (swap o split_last)
    1.23      end
    1.24  
    1.25 -  val with_extensions =
    1.26 -    Attrib.setup_config_bool @{binding z3_with_extensions} (K true)
    1.27 -
    1.28    fun select_class ctxt =
    1.29 -    if Config.get ctxt with_extensions then Z3_Interface.smtlib_z3C
    1.30 +    if Config.get ctxt z3_with_extensions then Z3_Interface.smtlib_z3C
    1.31      else SMTLIB_Interface.smtlibC
    1.32  
    1.33    fun mk is_remote = {