src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
changeset 50901 f4a6c360af35
parent 50786 af8ecf09a58c
child 50908 02ed5abcc0e5
equal deleted inserted replaced
50900:6d80709ab862 50901:f4a6c360af35
    66     local
    66     local
    67       open Unsynchronized
    67       open Unsynchronized
    68       val metis_fail = ref false
    68       val metis_fail = ref false
    69     in
    69     in
    70       fun handle_metis_fail try_metis () =
    70       fun handle_metis_fail try_metis () =
    71         try_metis () handle exp =>
    71         try_metis () handle exn =>
    72           (if Exn.is_interrupt exp orelse debug then reraise exp 
    72           (if Exn.is_interrupt exn orelse debug then reraise exn
    73            else metis_fail := true; SOME Time.zeroTime)
    73            else metis_fail := true; SOME Time.zeroTime)
    74       fun get_time lazy_time =
    74       fun get_time lazy_time =
    75         if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time
    75         if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time
    76       val metis_fail = fn () => !metis_fail
    76       val metis_fail = fn () => !metis_fail
    77     end
    77     end