updated 'old_smt' to loss of 'z3_non_commercial' option

--- a/src/HOL/Library/Old_SMT.thy	Wed Apr 08 19:15:55 2015 +0200
+++ b/src/HOL/Library/Old_SMT.thy	Wed Apr 08 19:19:02 2015 +0200
@@ -164,7 +164,8 @@
 
 Due to licensing restrictions, Yices and Z3 are not installed/enabled
 by default.  Z3 is free for non-commercial applications and can be enabled
-by setting Isabelle system option @{text z3_non_commercial} to @{text yes}.
+by setting the @{text OLD_Z3_NON_COMMERCIAL} environment variable to
+@{text yes}.
 *}
 
 declare [[ old_smt_solver = z3 ]]

--- 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