--- a/src/HOL/ex/Computations.thy Mon Feb 06 20:56:30 2017 +0100
+++ b/src/HOL/ex/Computations.thy Mon Feb 06 20:56:32 2017 +0100
@@ -30,14 +30,14 @@
val comp_nat = @{computation "0 :: nat" Suc
"plus :: nat \<Rightarrow>_" "times :: nat \<Rightarrow> _" fib :: nat}
- (fn post => post o HOLogic.mk_nat o int_of_nat);
+ (fn post => post o HOLogic.mk_nat o int_of_nat o the);
val comp_numeral = @{computation "0 :: nat" "1 :: nat" "2 :: nat" "3 :: nat" :: nat}
- (fn post => post o HOLogic.mk_nat o int_of_nat);
+ (fn post => post o HOLogic.mk_nat o int_of_nat o the);
val comp_bool = @{computation True False HOL.conj HOL.disj HOL.implies
HOL.iff even "less_eq :: nat \<Rightarrow> _" "less :: nat \<Rightarrow> _" "HOL.eq :: nat \<Rightarrow> _" :: bool }
- (K I);
+ (K the);
end
\<close>
--- a/src/Tools/Code/code_runtime.ML Mon Feb 06 20:56:30 2017 +0100
+++ b/src/Tools/Code/code_runtime.ML Mon Feb 06 20:56:32 2017 +0100
@@ -33,7 +33,7 @@
datatype truth = Holds
val put_truth: (unit -> truth) -> Proof.context -> Proof.context
val mount_computation: Proof.context -> (string * typ) list -> typ
- -> (term -> 'ml) -> ((term -> term) -> 'ml -> 'a) -> Proof.context -> term -> 'a
+ -> (term -> 'ml) -> ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
val trace: bool Config.T
end;
@@ -354,7 +354,8 @@
check_typ ctxt T
#> reject_vars ctxt
#> check_computation_input ctxt cTs
- #> raw_computation;
+ #> Exn.capture raw_computation
+ #> partiality_as_none;
fun mount_computation ctxt cTs T raw_computation lift_postproc =
Code_Preproc.static_value { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }