diff -r b4e7b9968e60 -r 8979b2463fc8 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Dec 01 20:54:48 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Dec 01 22:14:35 2011 +0100
@@ -297,8 +297,8 @@
       (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
     val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
     val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
-    val check = @{term "If :: bool => term list option => term list option => term list option"}
-      $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms);
+    val check = Quickcheck_Common.mk_safe_if ctxt (result, @{term "None :: term list option"},
+      @{term "Some :: term list => term list option"} $ terms)
     val return = @{term "Pair :: term list option => Random.seed => term list option * Random.seed"};
     fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
     fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"});
@@ -446,7 +446,6 @@
 val setup =
   Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
     (((@{sort typerep}, @{sort term_of}), @{sort random}), instantiate_random_datatype))
-  #> Code_Target.extend_target (target, (Code_Runtime.target, K I))
   #> Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals)));
 
 end;