--- a/src/HOL/ROOT Sun Sep 21 20:22:12 2014 +0200
+++ b/src/HOL/ROOT Mon Sep 22 10:18:41 2014 +0200
@@ -242,17 +242,17 @@
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 +