src/Tools/Code/code_runtime.ML
changeset 65005 3278831c226d
parent 64995 a7af4045f873
child 65034 1846c4551153
equal deleted inserted replaced
65004:fd4d1395fa17 65005:3278831c226d
   415   tap (check_typ ctxt T o reject_vars ctxt o Thm.term_of)
   415   tap (check_typ ctxt T o reject_vars ctxt o Thm.term_of)
   416   #> raw_conv ctxt;
   416   #> raw_conv ctxt;
   417 
   417 
   418 fun checked_computation cTs raw_computation ctxt =
   418 fun checked_computation cTs raw_computation ctxt =
   419   check_computation_input ctxt cTs
   419   check_computation_input ctxt cTs
   420   #> Exn.capture raw_computation
   420   #> Exn.interruptible_capture raw_computation
   421   #> partiality_as_none;
   421   #> partiality_as_none;
   422 
   422 
   423 fun mount_computation ctxt cTs T raw_computation lift_postproc =
   423 fun mount_computation ctxt cTs T raw_computation lift_postproc =
   424   let
   424   let
   425     val preprocess = preprocess_term { ctxt = ctxt };
   425     val preprocess = preprocess_term { ctxt = ctxt };