src/HOL/Import/replay.ML
changeset 41522 42d13d00ccfb
parent 41164 6854e9a40edc
child 43918 6ca79a354c51
     1.1 --- a/src/HOL/Import/replay.ML	Wed Jan 12 15:09:26 2011 +0100
     1.2 +++ b/src/HOL/Import/replay.ML	Wed Jan 12 15:15:51 2011 +0100
     1.3 @@ -275,7 +275,7 @@
     1.4          in
     1.5              x
     1.6          end
     1.7 -    end handle x => (ImportRecorder.abort_replay_proof thyname thmname; reraise x)
     1.8 +    end handle x => (ImportRecorder.abort_replay_proof thyname thmname; reraise x)  (* FIXME avoid handle x ?? *)
     1.9  
    1.10  fun setup_int_thms thyname thy =
    1.11      let