src/Tools/Code/code_runtime.ML

   val static_value_exn: 'a cookie -> { ctxt: Proof.context, target: string option,
     lift_postproc: (term -> term) -> 'a -> 'a, consts: string list }
     -> 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 }
     -> Proof.context -> term -> 'a Exn.result (*EXPERIMENTAL!*)
   val code_reflect: (string * string list option) list -> string list -> string

       lift_postproc = Exn.map_result o lift_postproc, consts = cs_code }
       (compile_evaluator cookie ctxt cs_code cTs T);
   in fn ctxt' =>
     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 **)
 
 local