--- a/src/Tools/Code/code_runtime.ML Sat Jan 08 16:01:51 2011 +0100
+++ b/src/Tools/Code/code_runtime.ML Sat Jan 08 17:14:48 2011 +0100
@@ -138,6 +138,7 @@
structure Truth_Result = Proof_Data
(
type T = unit -> truth
+ (* FIXME avoid user error with non-user text *)
fun init _ () = error "Truth_Result"
);
val put_truth = Truth_Result.put;
@@ -369,8 +370,8 @@
(
type T = string list
val empty = []
+ val extend = I
fun merge data : T = Library.merge (op =) data
- val extend = I
);
fun notify_val (string, value) =