--- a/src/HOL/Tools/quickcheck_generators.ML Tue Nov 10 15:33:35 2009 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML Tue Nov 10 16:04:57 2009 +0100
@@ -82,7 +82,7 @@
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
in
thy
- |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
+ |> Theory_Target.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
@@ -300,7 +300,7 @@
(HOLogic.mk_random T size, nth random_auxs k $ mk_size_arg k $ size)) Ts;
in
thy
- |> TheoryTarget.instantiation (tycos, vs, @{sort random})
+ |> Theory_Target.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 =>