--- a/src/Tools/Code/code_runtime.ML Thu Oct 09 17:31:50 2014 +0200
+++ b/src/Tools/Code/code_runtime.ML Thu Oct 09 16:47:56 2014 +0200
@@ -28,6 +28,14 @@
-> Proof.context -> term -> 'a Exn.result
val dynamic_holds_conv: Proof.context -> conv
val static_holds_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv
+ val static_value': (Proof.context -> term -> 'a) cookie
+ -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a,
+ consts: (string * typ) list, T: typ }
+ -> Proof.context -> term -> 'a option (*EXPERIMENTAL!*)
+ val static_value_strict': (Proof.context -> term -> 'a) cookie
+ -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a,
+ consts: (string * typ) list, T: typ }
+ -> Proof.context -> term -> 'a (*EXPERIMENTAL!*)
val static_value_exn': (Proof.context -> term -> 'a) cookie
-> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a,
consts: (string * typ) list, T: typ }
@@ -311,6 +319,10 @@
evaluator ctxt' o reject_vars ctxt' o Syntax.check_term ctxt' o Type.constraint T
end;
+fun static_value_strict' cookie = Exn.release ooo static_value_exn' cookie;
+
+fun static_value' cookie = partiality_as_none ooo static_value_exn' cookie;
+
(** code antiquotation **)