src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 42616 92715b528e78
parent 42361 23f352990944
child 43047 26774ccb1c74
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon May 02 16:33:21 2011 +0200
@@ -18,8 +18,7 @@
 
 (* configurations *)
 
-val (finite_functions, setup_finite_functions) =
-  Attrib.config_bool "quickcheck_finite_functions" (K true)
+val finite_functions = Attrib.setup_config_bool @{binding quickcheck_finite_functions} (K true)
 
 (* narrowing specific names and types *)
 
@@ -208,7 +207,6 @@
 val setup =
   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))