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