src/HOL/Tools/inductive_codegen.ML

 *)
 
 signature INDUCTIVE_CODEGEN =
 sig
   val add : string option -> int option -> attribute
-  val test_fn : (int * int * int -> term list option) Unsynchronized.ref
+  val test_fn : (int * int * int -> term list option) Unsynchronized.ref  (* FIXME *)
   val test_term:
     Proof.context -> term -> int -> term list option * Quickcheck.report option
   val setup : theory -> theory
   val quickcheck_setup : theory -> theory
 end;

             (map (fn (s, T) => Pretty.block
               [Codegen.mk_term_of gr "Generated" false T, Pretty.brk 1, Codegen.str s]) args'),
           Pretty.brk 1,
           Codegen.str "| NONE => NONE);"]) ^
       "\n\nend;\n";
-    val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;
+    val test_fn' = NAMED_CRITICAL "codegen" (fn () =>
+     (ML_Context.eval_text_in (SOME ctxt) false Position.none s; ! test_fn));
     val values = Config.get ctxt random_values;
     val bound = Config.get ctxt depth_bound;
     val start = Config.get ctxt depth_start;
     val offset = Config.get ctxt size_offset;
-    val test_fn' = !test_fn;
     fun test k = (deepen bound (fn i =>
       (Output.urgent_message ("Search depth: " ^ string_of_int i);
        test_fn' (i, values, k+offset))) start, NONE);
   in test end;