diff -r 7ec150fcf3dc -r 5611f178a747 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Wed Apr 20 14:33:33 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Wed Apr 20 15:55:34 2011 +0200
@@ -6,12 +6,12 @@
 
 signature INDUCTIVE_CODEGEN =
 sig
-  val add : string option -> int option -> attribute
-  val test_fn : (int * int * int -> term list option) Unsynchronized.ref  (* FIXME *)
-  val test_term:
-    Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
-  val setup : theory -> theory
-  val quickcheck_setup : theory -> theory
+  val add: string option -> int option -> attribute
+  val poke_test_fn: (int * int * int -> term list option) -> unit
+  val test_term: Proof.context -> (term * term list) list -> int list ->
+    term list option * Quickcheck.report option
+  val setup: theory -> theory
+  val quickcheck_setup: theory -> theory
 end;
 
 structure Inductive_Codegen : INDUCTIVE_CODEGEN =
@@ -792,10 +792,18 @@
       Scan.option (Args.$$$ "params" |-- Args.colon |-- Parse.nat) >> uncurry add))
     "introduction rules for executable predicates";
 
+
 (**** Quickcheck involving inductive predicates ****)
 
-val test_fn : (int * int * int -> term list option) Unsynchronized.ref =
-  Unsynchronized.ref (fn _ => NONE);
+structure Result = Proof_Data
+(
+  type T = int * int * int -> term list option;
+  fun init _ = (fn _ => NONE);
+);
+
+val get_test_fn = Result.get;
+fun poke_test_fn f = Context.>> (Context.map_proof (Result.put f));
+
 
 fun strip_imp p =
   let val (q, r) = HOLogic.dest_imp p
@@ -814,56 +822,61 @@
 val (size_offset, setup_size_offset) = Attrib.config_int "ind_quickcheck_size_offset" (K 0);
 
 fun test_term ctxt [(t, [])] =
-  let
-    val t' = list_abs_free (Term.add_frees t [], t)
-    val thy = Proof_Context.theory_of ctxt;
-    val (xs, p) = strip_abs t';
-    val args' = map_index (fn (i, (_, T)) => ("arg" ^ string_of_int i, T)) xs;
-    val args = map Free args';
-    val (ps, q) = strip_imp p;
-    val Ts = map snd xs;
-    val T = Ts ---> HOLogic.boolT;
-    val rl = Logic.list_implies
-      (map (HOLogic.mk_Trueprop o curry subst_bounds (rev args)) ps @
-       [HOLogic.mk_Trueprop (HOLogic.mk_not (subst_bounds (rev args, q)))],
-       HOLogic.mk_Trueprop (list_comb (Free ("quickcheckp", T), args)));
-    val (_, thy') = Inductive.add_inductive_global
-      {quiet_mode=true, verbose=false, alt_name=Binding.empty, coind=false,
-       no_elim=true, no_ind=false, skip_mono=false, fork_mono=false}
-      [((Binding.name "quickcheckp", T), NoSyn)] []
-      [(Attrib.empty_binding, rl)] [] (Theory.copy thy);
-    val pred = HOLogic.mk_Trueprop (list_comb
-      (Const (Sign.intern_const thy' "quickcheckp", T),
-       map Term.dummy_pattern Ts));
-    val (code, gr) =
-      Codegen.generate_code_i thy' ["term_of", "test", "random_ind"] [] "Generated"
-        [("testf", pred)];
-    val s = "structure TestTerm =\nstruct\n\n" ^
-      cat_lines (map snd code) ^
-      "\nopen Generated;\n\n" ^ Codegen.string_of
-        (Pretty.block [Codegen.str "val () = Inductive_Codegen.test_fn :=",
-          Pretty.brk 1, Codegen.str "(fn p =>", Pretty.brk 1,
-          Codegen.str "case Seq.pull (testf p) of", Pretty.brk 1,
-          Codegen.str "SOME ", mk_tuple [mk_tuple (map (Codegen.str o fst) args'), Codegen.str "_"],
-          Codegen.str " =>", Pretty.brk 1, Codegen.str "SOME ",
-          Pretty.enum "," "[" "]"
-            (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 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;
-    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
-  | test_term ctxt [(t, _)] = error "Option eval is not supported by tester SML_inductive"
-  | test_term ctxt _ = error "Compilation of multiple instances is not supported by tester SML_inductive";
+      let
+        val t' = list_abs_free (Term.add_frees t [], t)
+        val thy = Proof_Context.theory_of ctxt;
+        val (xs, p) = strip_abs t';
+        val args' = map_index (fn (i, (_, T)) => ("arg" ^ string_of_int i, T)) xs;
+        val args = map Free args';
+        val (ps, q) = strip_imp p;
+        val Ts = map snd xs;
+        val T = Ts ---> HOLogic.boolT;
+        val rl = Logic.list_implies
+          (map (HOLogic.mk_Trueprop o curry subst_bounds (rev args)) ps @
+           [HOLogic.mk_Trueprop (HOLogic.mk_not (subst_bounds (rev args, q)))],
+           HOLogic.mk_Trueprop (list_comb (Free ("quickcheckp", T), args)));
+        val (_, thy') = Inductive.add_inductive_global
+          {quiet_mode=true, verbose=false, alt_name=Binding.empty, coind=false,
+           no_elim=true, no_ind=false, skip_mono=false, fork_mono=false}
+          [((Binding.name "quickcheckp", T), NoSyn)] []
+          [(Attrib.empty_binding, rl)] [] (Theory.copy thy);
+        val pred = HOLogic.mk_Trueprop (list_comb
+          (Const (Sign.intern_const thy' "quickcheckp", T),
+           map Term.dummy_pattern Ts));
+        val (code, gr) =
+          Codegen.generate_code_i thy' ["term_of", "test", "random_ind"] [] "Generated"
+            [("testf", pred)];
+        val s = "structure Test_Term =\nstruct\n\n" ^
+          cat_lines (map snd code) ^
+          "\nopen Generated;\n\n" ^ Codegen.string_of
+            (Pretty.block [Codegen.str "val () = Inductive_Codegen.poke_test_fn",
+              Pretty.brk 1, Codegen.str "(fn p =>", Pretty.brk 1,
+              Codegen.str "case Seq.pull (testf p) of", Pretty.brk 1,
+              Codegen.str "SOME ",
+              mk_tuple [mk_tuple (map (Codegen.str o fst) args'), Codegen.str "_"],
+              Codegen.str " =>", Pretty.brk 1, Codegen.str "SOME ",
+              Pretty.enum "," "[" "]"
+                (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 test_fn =
+          ctxt
+          |> Context.proof_map
+              (ML_Context.exec (fn () => ML_Context.eval_text false Position.none s))
+          |> get_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;
+        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
+  | test_term ctxt [_] = error "Option eval is not supported by tester SML_inductive"
+  | test_term ctxt _ =
+      error "Compilation of multiple instances is not supported by tester SML_inductive";
 
 val quickcheck_setup =
   setup_depth_bound #>