--- a/src/HOL/Import/import_syntax.ML Tue Jul 12 16:00:05 2011 +0900
+++ b/src/HOL/Import/import_syntax.ML Wed Jul 13 00:23:24 2011 +0900
@@ -58,7 +58,7 @@
let
val _ = ImportRecorder.load_history thyname
val thy = Replay.import_thms thyname int_thms thmnames thy
- handle x => (ImportRecorder.save_history thyname; raise x) (* FIXME avoid handle x ?? *)
+ (*handle x => (ImportRecorder.save_history thyname; raise x)*) (* FIXME avoid handle x ?? *)
val _ = ImportRecorder.save_history thyname
val _ = ImportRecorder.clear_history ()
in