Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorbulwahn
Wed, 06 Apr 2011 13:08:44 +0200
changeset 42259 5ff3a11e18ca
parent 42258 79cb339d8989 (diff)
parent 42257 08d717c82828 (current diff)
child 42260 4ea47da3d19b
merged
--- 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))
isabelle