src/Tools/Code/code_runtime.ML
changeset 64988 93aaff2b0ae0
parent 64987 1985502518ce
child 64989 40c36a4aee1f
     1.1 --- a/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:30 2017 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:32 2017 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4    datatype truth = Holds
     1.5    val put_truth: (unit -> truth) -> Proof.context -> Proof.context
     1.6    val mount_computation: Proof.context -> (string * typ) list -> typ
     1.7 -    -> (term -> 'ml) -> ((term -> term) -> 'ml -> 'a) -> Proof.context -> term -> 'a
     1.8 +    -> (term -> 'ml) -> ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
     1.9    val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
    1.10    val trace: bool Config.T
    1.11  end;
    1.12 @@ -354,7 +354,8 @@
    1.13    check_typ ctxt T
    1.14    #> reject_vars ctxt
    1.15    #> check_computation_input ctxt cTs
    1.16 -  #> raw_computation;
    1.17 +  #> Exn.capture raw_computation
    1.18 +  #> partiality_as_none;
    1.19  
    1.20  fun mount_computation ctxt cTs T raw_computation lift_postproc =
    1.21    Code_Preproc.static_value { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }