eliminated global references / critical sections via context data;
misc tuning and modernization;

--- a/src/HOL/Library/SML_Quickcheck.thy	Wed Apr 20 14:33:33 2011 +0200
+++ b/src/HOL/Library/SML_Quickcheck.thy	Wed Apr 20 15:55:34 2011 +0200
@@ -11,17 +11,17 @@
     fn ctxt => fn [(t, eval_terms)] =>
       let
         val prop = list_abs_free (Term.add_frees t [], t)
-        val test_fun = Codegen.test_term ctxt prop 
+        val test_fun = Codegen.test_term ctxt prop
         val iterations = Config.get ctxt Quickcheck.iterations
         fun iterate size 0 = NONE
           | iterate size j =
-            let
-              val result = test_fun size handle Match => 
-                (if Config.get ctxt Quickcheck.quiet then ()
-                 else warning "Exception Match raised during quickcheck"; NONE)
-            in
-              case result of NONE => iterate size (j - 1) | SOME q => SOME q
-            end
+              let
+                val result = test_fun size handle Match =>
+                  (if Config.get ctxt Quickcheck.quiet then ()
+                   else warning "Exception Match raised during quickcheck"; NONE)
+              in
+                case result of NONE => iterate size (j - 1) | SOME q => SOME q
+              end
      in fn [_, size] => (iterate size iterations, NONE) end))
 *}
 

--- 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 #>

--- a/src/Pure/codegen.ML	Wed Apr 20 14:33:33 2011 +0200
+++ b/src/Pure/codegen.ML	Wed Apr 20 15:55:34 2011 +0200
@@ -74,9 +74,9 @@
   val mk_type: bool -> typ -> Pretty.T
   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  (* FIXME *)
+  val poke_test_fn: (int -> term list option) -> unit
+  val poke_eval_fn: (unit -> term) -> unit
   val test_term: Proof.context -> term -> int -> term list option
-  val eval_result: (unit -> term) Unsynchronized.ref  (* FIXME *)
   val eval_term: Proof.context -> term -> term
   val evaluation_conv: Proof.context -> conv
   val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
@@ -850,6 +850,21 @@
           [mk_term_of gr module true T, mk_type true T]) Ts)));
 
 
+(**** Implicit results ****)
+
+structure Result = Proof_Data
+(
+  type T = (int -> term list option) * (unit -> term);
+  fun init _ = (fn _ => NONE, fn () => Bound 0);
+);
+
+val get_test_fn = #1 o Result.get;
+val get_eval_fn = #2 o Result.get;
+
+fun poke_test_fn f = Context.>> (Context.map_proof (Result.map (fn (_, g) => (f, g))));
+fun poke_eval_fn g = Context.>> (Context.map_proof (Result.map (fn (f, _) => (f, g))));
+
+
 (**** Test data generators ****)
 
 fun mk_gen gr module p xs a (TVar ((s, i), _)) = str
@@ -867,19 +882,16 @@
               [mk_gen gr module true xs a T, mk_type true T]) Ts) @
          (if member (op =) xs s then [str a] else []))));
 
-val test_fn : (int -> term list option) Unsynchronized.ref =
-  Unsynchronized.ref (fn _ => NONE);
-
 fun test_term ctxt t =
   let
     val thy = Proof_Context.theory_of ctxt;
     val (code, gr) = generate_code_i thy ["term_of", "test"] [] "Generated" [("testf", t)];
     val Ts = map snd (fst (strip_abs t));
     val args = map_index (fn (i, T) => ("arg" ^ string_of_int i, T)) Ts;
-    val s = "structure TestTerm =\nstruct\n\n" ^
+    val s = "structure Test_Term =\nstruct\n\n" ^
       cat_lines (map snd code) ^
       "\nopen Generated;\n\n" ^ string_of
-        (Pretty.block [str "val () = Codegen.test_fn :=",
+        (Pretty.block [str "val () = Codegen.poke_test_fn",
           Pretty.brk 1, str ("(fn i =>"), Pretty.brk 1,
           mk_let (map (fn (s, T) =>
               (mk_tuple [str s, str (s ^ "_t")],
@@ -893,42 +905,39 @@
                 Pretty.enum "," "[" "]" (map (fn (s, _) => str (s ^ "_t ()")) args)]]),
           str ");"]) ^
       "\n\nend;\n";
-    val test_fn' = NAMED_CRITICAL "codegen" (fn () =>
-      (ML_Context.eval_text_in (SOME ctxt) false Position.none s; ! test_fn));
-  in test_fn' end;
-
+  in
+    ctxt
+    |> Context.proof_map (ML_Context.exec (fn () => ML_Context.eval_text false Position.none s))
+    |> get_test_fn
+  end;
 
 
 (**** Evaluator for terms ****)
 
-val eval_result = Unsynchronized.ref (fn () => Bound 0);
-
 fun eval_term ctxt t =
   let
-    val e =
-      let
-        val thy = Proof_Context.theory_of ctxt;
-        val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
-          error "Term to be evaluated contains type variables";
-        val _ = (null (Term.add_vars t []) andalso null (Term.add_frees t [])) orelse
-          error "Term to be evaluated contains variables";
-        val (code, gr) =
-          generate_code_i thy ["term_of"] [] "Generated"
-            [("result", Abs ("x", TFree ("'a", []), t))];
-        val s = "structure EvalTerm =\nstruct\n\n" ^
-          cat_lines (map snd code) ^
-          "\nopen Generated;\n\n" ^ string_of
-            (Pretty.block [str "val () = Codegen.eval_result := (fn () =>",
-              Pretty.brk 1,
-              mk_app false (mk_term_of gr "Generated" false (fastype_of t))
-                [str "(result ())"],
-              str ");"]) ^
-          "\n\nend;\n";
-      in
-        NAMED_CRITICAL "codegen" (fn () =>
-         (ML_Context.eval_text_in (SOME ctxt) false Position.none s; ! eval_result))
-      end
-  in e () end;
+    val thy = Proof_Context.theory_of ctxt;
+    val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
+      error "Term to be evaluated contains type variables";
+    val _ = (null (Term.add_vars t []) andalso null (Term.add_frees t [])) orelse
+      error "Term to be evaluated contains variables";
+    val (code, gr) =
+      generate_code_i thy ["term_of"] [] "Generated"
+        [("result", Abs ("x", TFree ("'a", []), t))];
+    val s = "structure Eval_Term =\nstruct\n\n" ^
+      cat_lines (map snd code) ^
+      "\nopen Generated;\n\n" ^ string_of
+        (Pretty.block [str "val () = Codegen.poke_eval_fn (fn () =>",
+          Pretty.brk 1,
+          mk_app false (mk_term_of gr "Generated" false (fastype_of t))
+            [str "(result ())"],
+          str ");"]) ^
+      "\n\nend;\n";
+    val eval_fn =
+      ctxt
+      |> Context.proof_map (ML_Context.exec (fn () => ML_Context.eval_text false Position.none s))
+      |> get_eval_fn;
+  in eval_fn () end;
 
 val (_, evaluation_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (Binding.name "evaluation", fn (ctxt, ct) =>