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