# HG changeset patch # User bulwahn # Date 1302088124 -7200 # Node ID 5ff3a11e18caace5617c7d027e96658fa2f94557 # Parent 79cb339d898936a8da373c4b108090b5852af8d5# Parent 08d717c828282fd4113ab264e0964cba2699323a merged diff -r 08d717c82828 -r 5ff3a11e18ca src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue Apr 05 19:55:04 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Apr 06 13:08:44 2011 +0200 @@ -206,8 +206,8 @@ val setup = - Datatype.interpretation - (Quickcheck_Common.ensure_sort_datatype (@{sort narrowing}, instantiate_narrowing_datatype)) + Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype + (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype)) #> setup_finite_functions #> Context.theory_map (Quickcheck.add_generator ("narrowing", compile_generator_expr))