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 **)