# HG changeset patch # User bulwahn # Date 1302080298 -7200 # Node ID 79cb339d898936a8da373c4b108090b5852af8d5 # Parent e48baf91aeabfe1afe8ff93fa19b0695b2bd3450 changing ensure_sort_datatype call in narrowing quickcheck (missed in 1491b7209e76) diff -r e48baf91aeab -r 79cb339d8989 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue Apr 05 15:15:33 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Apr 06 10:58:18 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))