src/Tools/Code/code_runtime.ML
changeset 39820 cd691e2c7a1a
parent 39816 c7cec137c48a
child 39913 721ba2c1a799
--- 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
 );