src/HOL/Library/Old_SMT/old_smt_setup_solvers.ML

--- a/src/HOL/Library/Old_SMT/old_smt_setup_solvers.ML	Wed Apr 08 19:15:55 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_setup_solvers.ML	Wed Apr 08 19:19:02 2015 +0200
@@ -99,12 +99,9 @@
 
 fun z3_non_commercial () =
   let
-    val flag1 = Options.default_string @{system_option z3_non_commercial}
-    val flag2 = getenv "Z3_NON_COMMERCIAL"
+    val flag2 = getenv "OLD_Z3_NON_COMMERCIAL"
   in
-    if accepted flag1 then Z3_Non_Commercial_Accepted
-    else if declined flag1 then Z3_Non_Commercial_Declined
-    else if accepted flag2 then Z3_Non_Commercial_Accepted
+    if accepted flag2 then Z3_Non_Commercial_Accepted
     else if declined flag2 then Z3_Non_Commercial_Declined
     else Z3_Non_Commercial_Unknown
   end