src/Tools/Code/code_runtime.ML
changeset 62607 43d282be7350
parent 62495 83db706d7771
child 62716 d80b9f4990e4
     1.1 --- a/src/Tools/Code/code_runtime.ML	Sat Mar 12 22:51:37 2016 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Sun Mar 13 09:06:50 2016 +0100
     1.3 @@ -52,7 +52,6 @@
     1.4  struct
     1.5  
     1.6  open Basic_Code_Symbol;
     1.7 -open Basic_Code_Thingol;
     1.8  
     1.9  (** evaluation **)
    1.10  
    1.11 @@ -324,10 +323,6 @@
    1.12  
    1.13  fun static_value' cookie = partiality_as_none ooo static_value_exn' cookie;
    1.14  
    1.15 -fun static_value_strict' cookie = Exn.release ooo static_value_exn' cookie;
    1.16 -
    1.17 -fun static_value' cookie = partiality_as_none ooo static_value_exn' cookie;
    1.18 -
    1.19  
    1.20  (** code antiquotation **)
    1.21