src/Tools/Code/code_runtime.ML
changeset 41472 f6ab14e61604
parent 41376 08240feb69c7
child 41486 82c1e348bc18
     1.1 --- a/src/Tools/Code/code_runtime.ML	Sat Jan 08 16:01:51 2011 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Sat Jan 08 17:14:48 2011 +0100
     1.3 @@ -138,6 +138,7 @@
     1.4  structure Truth_Result = Proof_Data
     1.5  (
     1.6    type T = unit -> truth
     1.7 +  (* FIXME avoid user error with non-user text *)
     1.8    fun init _ () = error "Truth_Result"
     1.9  );
    1.10  val put_truth = Truth_Result.put;
    1.11 @@ -369,8 +370,8 @@
    1.12  (
    1.13    type T = string list
    1.14    val empty = []
    1.15 +  val extend = I
    1.16    fun merge data : T = Library.merge (op =) data
    1.17 -  val extend = I
    1.18  );
    1.19  
    1.20  fun notify_val (string, value) =