tuned;
authorwenzelm
Fri, 21 Mar 2014 12:14:33 +0100
changeset 56242 d0a9100a5a38
parent 56241 029246729dc0
child 56243 2e10a36b8d46
tuned;
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 **)