src/HOL/Import/import_syntax.ML
changeset 41522 42d13d00ccfb
parent 40526 ca3c6b1bfcdb
child 43785 2bd54d4b5f3d
     1.1 --- a/src/HOL/Import/import_syntax.ML	Wed Jan 12 15:09:26 2011 +0100
     1.2 +++ b/src/HOL/Import/import_syntax.ML	Wed Jan 12 15:15:51 2011 +0100
     1.3 @@ -58,7 +58,7 @@
     1.4                      let
     1.5                          val _ = ImportRecorder.load_history thyname
     1.6                          val thy = Replay.import_thms thyname int_thms thmnames thy
     1.7 -                            handle x => (ImportRecorder.save_history thyname; raise x)
     1.8 +                            handle x => (ImportRecorder.save_history thyname; raise x)  (* FIXME avoid handle x ?? *)
     1.9                          val _ = ImportRecorder.save_history thyname
    1.10                          val _ = ImportRecorder.clear_history ()
    1.11                      in