dropped junk
authorhaftmann
Sun, 13 Mar 2016 09:06:50 +0100
changeset 62607 43d282be7350
parent 62606 247963aa1c5d
child 62608 19f87fa0cfcb
dropped junk
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 **)