reverted some odd changes to HOL/Import (cf. 74c08021ab2e);

--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Mon Aug 22 10:57:33 2011 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Mon Aug 22 12:17:22 2011 +0200
@@ -28,12 +28,11 @@
   TYPE_DEFINITION > HOL4Setup.TYPE_DEFINITION
   LET             > HOL4Compat.LET;
 
-(*ignore_thms
+ignore_thms
   BOUNDED_DEF
   BOUNDED_THM
   UNBOUNDED_DEF
   UNBOUNDED_THM;
-*)
 
 end_import;
 

--- a/src/HOL/Import/Generate-HOL/ROOT.ML	Mon Aug 22 10:57:33 2011 +0200
+++ b/src/HOL/Import/Generate-HOL/ROOT.ML	Mon Aug 22 12:17:22 2011 +0200
@@ -1,5 +1,3 @@
-Runtime.debug := true;
-
 use_thy "GenHOL4Prob";
 use_thy "GenHOL4Vec";
 use_thy "GenHOL4Word32";