--- a/src/HOL/ex/ROOT.ML Thu Sep 25 10:17:23 2008 +0200
+++ b/src/HOL/ex/ROOT.ML Thu Sep 25 11:14:01 2008 +0200
@@ -18,7 +18,7 @@
];
no_document use_thy "Codegenerator";
-(*no_document use_thy "Codegenerator_Pretty";*)
+no_document use_thy "Codegenerator_Pretty";
use_thys [
"Numeral",