src/Tools/Code/code_runtime.ML

   partiality_as_none (static_value_exn cookie thy some_target postproc consts t);
 
 
 (* evaluation for truth or nothing *)
 
-structure Truth_Result = Proof_Data (
+structure Truth_Result = Proof_Data
+(
   type T = unit -> truth
   fun init _ () = error "Truth_Result"
 );
 val put_truth = Truth_Result.put;
 val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth");

 
 (** using external SML files as substitute for proper definitions -- only for polyml!  **)
 
 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
 );
 
 fun notify_val (string, value) = 
   let