src/Tools/Code/code_runtime.ML
changeset 65005 3278831c226d
parent 64995 a7af4045f873
child 65034 1846c4551153
     1.1 --- a/src/Tools/Code/code_runtime.ML	Wed Feb 08 23:19:10 2017 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Wed Feb 08 22:26:10 2017 +0100
     1.3 @@ -417,7 +417,7 @@
     1.4  
     1.5  fun checked_computation cTs raw_computation ctxt =
     1.6    check_computation_input ctxt cTs
     1.7 -  #> Exn.capture raw_computation
     1.8 +  #> Exn.interruptible_capture raw_computation
     1.9    #> partiality_as_none;
    1.10  
    1.11  fun mount_computation ctxt cTs T raw_computation lift_postproc =