disable hard-to-reconstruct Z3 feature

--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Jun 03 14:38:41 2014 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Jun 03 16:02:41 2014 +0200
@@ -174,13 +174,11 @@
 
 lemma
   "a \<noteq> b \<and> a \<noteq> c \<and> b \<noteq> c \<and> (\<forall>x y. f x = f y \<longrightarrow> y = x) \<longrightarrow> f a \<noteq> f b"
-  using [[smt2_oracle=true]] (* FIXME: disable refine_inj_axiom in Z3 *)
   by smt2
 
 lemma
   "(\<forall>x y z. f x y = f x z \<longrightarrow> y = z) \<and> b \<noteq> c \<longrightarrow> f a b \<noteq> f a c"
   "(\<forall>x y z. f x y = f z y \<longrightarrow> x = z) \<and> a \<noteq> d \<longrightarrow> f a b \<noteq> f d b"
-  using [[smt2_oracle=true]] (* FIXME: disable refine_inj_axiom in Z3 *)
   by smt2+
 
 

--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Tue Jun 03 14:38:41 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Tue Jun 03 16:02:41 2014 +0200
@@ -125,6 +125,7 @@
 
   fun z3_options ctxt =
     ["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
+     "smt.refine_inj_axioms=false",
      "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)),
      "-smt2"]