do not hardwire document output options -- to be provided by the user;

--- a/src/HOL/ROOT	Tue Aug 28 17:57:47 2012 +0200
+++ b/src/HOL/ROOT	Tue Aug 28 18:46:15 2012 +0200
@@ -605,9 +605,11 @@
 session "HOL-Ordinals_and_Cardinals" in Ordinals_and_Cardinals =
     "HOL-Ordinals_and_Cardinals-Base" +
   description {* Ordinals and Cardinals, Full Theories *}
-  options [document = pdf, document_output = "."]
   theories Cardinal_Order_Relation
-  files "document/intro.tex" "document/root.tex" "document/root.bib"
+  files
+    "document/intro.tex"
+    "document/root.tex"
+    "document/root.bib"
 
 session "HOL-Codatatype" in Codatatype = "HOL-Ordinals_and_Cardinals-Base" +
   description {* New (Co)datatype Package *}