diff -r 19000bb11ff5 -r cf7b2121ad9d src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Wed Aug 11 14:31:43 2010 +0200
@@ -86,7 +86,7 @@
     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   in   
     thy
-    |> Theory_Target.instantiation ([tyco], vs, @{sort random})
+    |> Class.instantiation ([tyco], vs, @{sort random})
     |> `(fn lthy => Syntax.check_term lthy eq)
     |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
     |> snd
@@ -304,7 +304,7 @@
       (HOLogic.mk_random T size, nth random_auxs k $ mk_size_arg k $ size)) Ts;
   in
     thy
-    |> Theory_Target.instantiation (tycos, vs, @{sort random})
+    |> Class.instantiation (tycos, vs, @{sort random})
     |> random_aux_specification prfx random_auxN auxs_eqs
     |> `(fn lthy => map (Syntax.check_term lthy) random_defs)
     |-> (fn random_defs' => fold_map (fn random_def =>