--- a/src/Pure/codegen.ML Tue Feb 23 16:58:21 2010 +0100
+++ b/src/Pure/codegen.ML Thu Feb 25 09:28:01 2010 +0100
@@ -76,7 +76,7 @@
val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
val test_fn: (int -> term list option) Unsynchronized.ref
- val test_term: Proof.context -> term -> int -> term list option
+ val test_term: Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
val eval_result: (unit -> term) Unsynchronized.ref
val eval_term: theory -> term -> term
val evaluation_conv: cterm -> thm
@@ -871,7 +871,7 @@
val test_fn : (int -> term list option) Unsynchronized.ref =
Unsynchronized.ref (fn _ => NONE);
-fun test_term ctxt t =
+fun test_term ctxt report t =
let
val thy = ProofContext.theory_of ctxt;
val (code, gr) = setmp_CRITICAL mode ["term_of", "test"]
@@ -897,7 +897,8 @@
str ");"]) ^
"\n\nend;\n";
val _ = ML_Context.eval_in (SOME ctxt) false Position.none s;
- in ! test_fn end;
+ val dummy_report = ([], false)
+ in (fn size => (! test_fn size, dummy_report)) end;