# HG changeset patch
# User obua
# Date 1127717421 -7200
# Node ID 7568d2cc560e48af29b4177c9a60e8d3585c330a
# Parent  bcf00e7b251b393f3f0d386c17f317c0589b529d
tuned

diff -r bcf00e7b251b -r 7568d2cc560e src/HOL/Import/HOL/ROOT.ML
--- a/src/HOL/Import/HOL/ROOT.ML	Mon Sep 26 08:49:50 2005 +0200
+++ b/src/HOL/Import/HOL/ROOT.ML	Mon Sep 26 08:50:21 2005 +0200
@@ -3,6 +3,5 @@
     Author:     Sebastian Skalberg (TU Muenchen)
 *)
 
-set show_types; set show_sorts;
 use_thy "HOL4Prob";
 use_thy "HOL4";