diff -r 247963aa1c5d -r 43d282be7350 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Sat Mar 12 22:51:37 2016 +0100
+++ b/src/Tools/Code/code_runtime.ML	Sun Mar 13 09:06:50 2016 +0100
@@ -52,7 +52,6 @@
 struct
 
 open Basic_Code_Symbol;
-open Basic_Code_Thingol;
 
 (** evaluation **)
 
@@ -324,10 +323,6 @@
 
 fun static_value' cookie = partiality_as_none ooo static_value_exn' cookie;
 
-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 **)