# HG changeset patch # User bulwahn # Date 1302273074 -7200 # Node ID 8dfb7878a3511f86dc79936bd8386ad13b3de4c1 # Parent d0bea229a9ce066a9ad09434620bbe7d84c5a50a correcting constant name in exhaustive_generators diff -r d0bea229a9ce -r 8dfb7878a351 src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Apr 08 16:31:14 2011 +0200 @@ -422,7 +422,7 @@ $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) $ lambda free (lambda term_var t)) else - Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T) + Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, full_exhaustiveT T) $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) $ lambda free (lambda term_var t)) $ depth val none_t = @{term "None :: term list option"}