changing ensure_sort_datatype call in narrowing quickcheck (missed in 1491b7209e76)
authorbulwahn
Wed Apr 06 10:58:18 2011 +0200 (2011-04-06)
changeset 4225879cb339d8989
parent 42239 e48baf91aeab
child 42259 5ff3a11e18ca
changing ensure_sort_datatype call in narrowing quickcheck (missed in 1491b7209e76)
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Apr 05 15:15:33 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Apr 06 10:58:18 2011 +0200
     1.3 @@ -206,8 +206,8 @@
     1.4  
     1.5  
     1.6  val setup =
     1.7 -  Datatype.interpretation
     1.8 -    (Quickcheck_Common.ensure_sort_datatype (@{sort narrowing}, instantiate_narrowing_datatype))
     1.9 +  Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
    1.10 +    (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype))
    1.11    #> setup_finite_functions
    1.12    #> Context.theory_map
    1.13      (Quickcheck.add_generator ("narrowing", compile_generator_expr))