diff -r bf5b45870110 -r a7eed34cf219 src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Jul 25 10:55:02 2012 +0200
+++ b/src/HOL/ROOT	Wed Jul 25 11:59:22 2012 +0200
@@ -290,7 +290,7 @@
   files "document/root.bib" "document/root.tex"
 
 session Decision_Procs = HOL +
-  options [document = false]
+  options [condition = ISABELLE_POLYML, document = false]
   theories Decision_Procs
 
 session ex in "Proofs/ex" = "HOL-Proofs" +
@@ -299,7 +299,7 @@
 
 session Extraction in "Proofs/Extraction" = "HOL-Proofs" +
   description {* Examples for program extraction in Higher-Order Logic *}
-  options [proofs = 2, parallel_proofs = 0]
+  options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0]
   theories [document = false]
     "~~/src/HOL/Library/Efficient_Nat"
     "~~/src/HOL/Library/Monad_Syntax"
@@ -395,6 +395,7 @@
 
 session ex = HOL +
   description {* Miscellaneous examples for Higher-Order Logic. *}
+  options [condition = ISABELLE_POLYML]
   theories [document = false]
     "~~/src/HOL/Library/State_Monad"
     Code_Nat_examples
@@ -559,7 +560,7 @@
     "document/root.tex"
 
 session "HOL-Probability"! in "Probability" = "HOL-Multivariate_Analysis" +
-  options [document_graph]
+  options [condition = ISABELLE_POLYML, document_graph]
   theories [document = false]
     "~~/src/HOL/Library/Countable"
     "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
@@ -575,7 +576,7 @@
   theories Nominal
 
 session Examples in "Nominal/Examples" = "HOL-Nominal" +
-  options [document = false]
+  options [condition = ISABELLE_POLYML, document = false]
   theories Nominal_Examples
   theories [quick_and_dirty] VC_Condition