# HG changeset patch
# User haftmann
# Date 1330810691 -3600
# Node ID 074dc33767a5b4cd07d56f39e4550bccc0a53ddf
# Parent  aefdc0095d7ead83bfed8f6116f22e5859ebe631
turn on quick and dirty in batch mode

diff -r aefdc0095d7e -r 074dc33767a5 src/HOL/Import/HOL4/imported.ML
--- a/src/HOL/Import/HOL4/imported.ML	Sat Mar 03 22:37:56 2012 +0100
+++ b/src/HOL/Import/HOL4/imported.ML	Sat Mar 03 22:38:11 2012 +0100
@@ -1,2 +1,2 @@
 
-use_thy "Imported";
+Unsynchronized.setmp quick_and_dirty true use_thy "Imported";
diff -r aefdc0095d7e -r 074dc33767a5 src/HOL/Import/HOL_Light/imported.ML
--- a/src/HOL/Import/HOL_Light/imported.ML	Sat Mar 03 22:37:56 2012 +0100
+++ b/src/HOL/Import/HOL_Light/imported.ML	Sat Mar 03 22:38:11 2012 +0100
@@ -1,2 +1,2 @@
 
-use_thy "Imported";
+Unsynchronized.setmp quick_and_dirty true use_thy "Imported";