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";