--- a/src/Tools/Code/code_runtime.ML Fri Oct 01 16:44:13 2010 +0200
+++ b/src/Tools/Code/code_runtime.ML Fri Oct 01 17:23:26 2010 +0200
@@ -121,7 +121,8 @@
(* evaluation for truth or nothing *)
-structure Truth_Result = Proof_Data (
+structure Truth_Result = Proof_Data
+(
type T = unit -> truth
fun init _ () = error "Truth_Result"
);
@@ -347,10 +348,11 @@
local
-structure Loaded_Values = Theory_Data(
+structure Loaded_Values = Theory_Data
+(
type T = string list
val empty = []
- val merge = merge (op =)
+ fun merge data : T = Library.merge (op =) data
val extend = I
);