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