Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 42258 79cb339d8989
parent 42214 9ca13615c619
child 42361 23f352990944 
--- 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))
isabelle