src/HOL/ROOT

     Generate_Binary_Nat
     Generate_Target_Nat
     Generate_Efficient_Datastructures
     Generate_Pretty_Char
     Code_Test
-  theories[condition = ISABELLE_GHC]
+  theories [condition = ISABELLE_GHC]
     Code_Test_GHC
-  theories[condition = ISABELLE_MLTON]
+  theories [condition = ISABELLE_MLTON]
     Code_Test_MLton
-  theories[condition = ISABELLE_OCAMLC]
+  theories [condition = ISABELLE_OCAMLC]
     Code_Test_OCaml
-  theories[condition = ISABELLE_POLYML_PATH]
+  theories [condition = ISABELLE_POLYML]
     Code_Test_PolyML
-  theories[condition = ISABELLE_SCALA]
+  theories [condition = ISABELLE_SCALA]
     Code_Test_Scala
-  theories[condition = ISABELLE_SMLNJ]
+  theories [condition = ISABELLE_SMLNJ]
     Code_Test_SMLNJ
 
 session "HOL-Metis_Examples" in Metis_Examples = HOL +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory