src/Tools/Code/code_runtime.ML
changeset 58645 94bef115c08f
parent 58643 133203bd474b
child 59104 a14475f044b2
     1.1 --- a/src/Tools/Code/code_runtime.ML	Fri Oct 10 18:23:59 2014 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Thu Oct 09 22:43:48 2014 +0200
     1.3 @@ -323,6 +323,10 @@
     1.4  
     1.5  fun static_value' cookie = partiality_as_none ooo static_value_exn' cookie;
     1.6  
     1.7 +fun static_value_strict' cookie = Exn.release ooo static_value_exn' cookie;
     1.8 +
     1.9 +fun static_value' cookie = partiality_as_none ooo static_value_exn' cookie;
    1.10 +
    1.11  
    1.12  (** code antiquotation **)
    1.13