# HG changeset patch
# User haftmann
# Date 1222330643 -7200
# Node ID cab797b7942143f94b05f822e18d9632c42ac0cb
# Parent  abfc66969d1f0f6738f859ecb3c3a797c4ee2e66
(temporal deactivation)

diff -r abfc66969d1f -r cab797b79421 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Thu Sep 25 10:17:22 2008 +0200
+++ b/src/HOL/ex/ROOT.ML	Thu Sep 25 10:17:23 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",