src/HOL/ROOT

--- a/src/HOL/ROOT	Fri Dec 19 23:33:08 2014 +0100
+++ b/src/HOL/ROOT	Sat Dec 20 00:05:20 2014 +0100
@@ -725,9 +725,26 @@
 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
   options [condition = ML_SYSTEM_POLYML, document = false]
   theories
-    Nominal_Examples_Base
-  theories [condition = ISABELLE_FULL_TEST]
-    Nominal_Examples
+    Class3
+    CK_Machine
+    Compile
+    Contexts
+    Crary
+    CR_Takahashi
+    CR
+    Fsub
+    Height
+    Lambda_mu
+    Lam_Funs
+    LocalWeakening
+    Pattern
+    SN
+    SOS
+    Standardization
+    Support
+    Type_Preservation
+    Weakening
+    W
   theories [quick_and_dirty]
     VC_Condition