src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 56242 d0a9100a5a38
parent 56135 efa24d31e595
child 56920 d651b944c67e
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 21 11:42:32 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 21 12:14:33 2014 +0100
@@ -34,7 +34,7 @@
 fun mk_partial_term_of (x, T) =
   Const (@{const_name Quickcheck_Narrowing.partial_term_of_class.partial_term_of},
     Term.itselfT T --> @{typ narrowing_term} --> @{typ Code_Evaluation.term})
-      $ Const ("TYPE", Term.itselfT T) $ x
+      $ Logic.mk_type T $ x
 
 (** formal definition **)