# HG changeset patch
# User wenzelm
# Date 1314008242 -7200
# Node ID d3e609c87c4ce75cee2d87ddb2933aff2ef5f246
# Parent  9c5cc8134cba3b43904a872089000a9cc4ec73fb
reverted some odd changes to HOL/Import (cf. 74c08021ab2e);

diff -r 9c5cc8134cba -r d3e609c87c4c src/HOL/Import/Generate-HOL/GenHOL4Base.thy
--- 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;
 
diff -r 9c5cc8134cba -r d3e609c87c4c src/HOL/Import/Generate-HOL/ROOT.ML
--- 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";