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