# HG changeset patch
# User wenzelm
# Date 1411323732 -7200
# Node ID 22dd971f6938bfd00dce20951f8bd3b70896c0f2
# Parent  f65f11f4854c4a8dfffceac79c4505f5a6f85c0b
renamed ISABELLE_POLYML to ML_SYSTEM_POLYML, to avoid overlap with ISABELLE_POLYML_PATH;

diff -r f65f11f4854c -r 22dd971f6938 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Sun Sep 21 20:14:04 2014 +0200
+++ b/lib/scripts/getsettings	Sun Sep 21 20:22:12 2014 +0200
@@ -260,10 +260,10 @@
 #build condition etc.
 case "$ML_SYSTEM" in
   polyml*)
-    ISABELLE_POLYML="true"
+    ML_SYSTEM_POLYML="true"
     ;;
   *)
-    ISABELLE_POLYML=""
+    ML_SYSTEM_POLYML=""
     ;;
 esac
 
diff -r f65f11f4854c -r 22dd971f6938 src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Sun Sep 21 20:14:04 2014 +0200
+++ b/src/Doc/System/Basics.thy	Sun Sep 21 20:22:12 2014 +0200
@@ -217,7 +217,7 @@
   automatically obtained by composing the values of @{setting
   ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values.
 
-  \item[@{setting_def ISABELLE_POLYML}@{text "\<^sup>*"}] is @{verbatim true}
+  \item[@{setting_def ML_SYSTEM_POLYML}@{text "\<^sup>*"}] is @{verbatim true}
   for @{setting ML_SYSTEM} values derived from Poly/ML, as opposed to
   SML/NJ where it is empty.  This is particularly useful with the
   build option @{system_option condition}
diff -r f65f11f4854c -r 22dd971f6938 src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Sep 21 20:14:04 2014 +0200
+++ b/src/HOL/ROOT	Sun Sep 21 20:22:12 2014 +0200
@@ -388,7 +388,7 @@
   description {*
     Various decision procedures, typically involving reflection.
   *}
-  options [condition = ISABELLE_POLYML, document = false]
+  options [condition = ML_SYSTEM_POLYML, document = false]
   theories Decision_Procs
 
 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
@@ -401,7 +401,7 @@
   description {*
     Examples for program extraction in Higher-Order Logic.
   *}
-  options [condition = ISABELLE_POLYML, parallel_proofs = 0]
+  options [condition = ML_SYSTEM_POLYML, parallel_proofs = 0]
   theories [document = false]
     "~~/src/HOL/Library/Code_Target_Numeral"
     "~~/src/HOL/Library/Monad_Syntax"
@@ -524,7 +524,7 @@
   description {*
     Miscellaneous examples for Higher-Order Logic.
   *}
-  options [timeout = 3600, condition = ISABELLE_POLYML]
+  options [timeout = 3600, condition = ML_SYSTEM_POLYML]
   theories [document = false]
     "~~/src/HOL/Library/State_Monad"
     Code_Binary_Nat_examples
@@ -719,7 +719,7 @@
   theories Nominal
 
 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
-  options [timeout = 3600, condition = ISABELLE_POLYML, document = false]
+  options [timeout = 3600, condition = ML_SYSTEM_POLYML, document = false]
   theories
     Nominal_Examples_Base
   theories [condition = ISABELLE_FULL_TEST]
diff -r f65f11f4854c -r 22dd971f6938 src/Tools/ROOT
--- a/src/Tools/ROOT	Sun Sep 21 20:14:04 2014 +0200
+++ b/src/Tools/ROOT	Sun Sep 21 20:22:12 2014 +0200
@@ -1,11 +1,11 @@
 session Spec_Check in Spec_Check = Pure +
   theories
     Spec_Check
-  theories [condition = ISABELLE_POLYML]
+  theories [condition = ML_SYSTEM_POLYML]
     Examples
 
 session SML in SML = Pure +
-  options [condition = ISABELLE_POLYML]
+  options [condition = ML_SYSTEM_POLYML]
   theories
     Examples