src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 42258 79cb339d8989
parent 42214 9ca13615c619
child 42361 23f352990944
equal deleted inserted replaced
42239:e48baf91aeab 42258:79cb339d8989
   204     (result, NONE)
   204     (result, NONE)
   205   end;
   205   end;
   206 
   206 
   207 
   207 
   208 val setup =
   208 val setup =
   209   Datatype.interpretation
   209   Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
   210     (Quickcheck_Common.ensure_sort_datatype (@{sort narrowing}, instantiate_narrowing_datatype))
   210     (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype))
   211   #> setup_finite_functions
   211   #> setup_finite_functions
   212   #> Context.theory_map
   212   #> Context.theory_map
   213     (Quickcheck.add_generator ("narrowing", compile_generator_expr))
   213     (Quickcheck.add_generator ("narrowing", compile_generator_expr))
   214     
   214     
   215 end;
   215 end;