equal
deleted
inserted
replaced
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 }; |