src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
changeset 56090 34bd10a9a2ad
parent 56083 b5d1d9c60341
child 56094 2adbc6e4cd8f
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -122,7 +122,7 @@
            |> Config.put SMT2_Config.infer_triggers (Config.get ctxt smt2_triggers)
            |> not (Config.get ctxt smt2_builtins)
               ? (SMT2_Builtin.filter_builtins is_boring_builtin_typ
-                 #> Config.put SMT2_Setup_Solvers.z3_extensions false)
+                 #> Config.put SMT2_Systems.z3_extensions false)
            |> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances
                 default_max_new_mono_instances