diff -r 6ddbd932fc00 -r cd691e2c7a1a src/Tools/Code/code_runtime.ML
--- 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
 );