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.
changing ensure_sort_datatype call in narrowing quickcheck (missed in 1491b7209e76)
authorbulwahn
Wed, 06 Apr 2011 10:58:18 +0200
changeset 42258 79cb339d8989
parent 42239 e48baf91aeab
child 42259 5ff3a11e18ca
changing ensure_sort_datatype call in narrowing quickcheck (missed in 1491b7209e76)
src/HOL/Tools/Quickcheck/narrowing_generators.ML file | annotate | diff | comparison | revisions 
--- 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