# HG changeset patch
# User wenzelm
# Date 1395400473 -3600
# Node ID d0a9100a5a38287092cc96e24c0d0832cc9bd9e0
# Parent  029246729dc09baa0afedcb7d2a8b538a172e766
tuned;

diff -r 029246729dc0 -r d0a9100a5a38 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- 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 **)