# 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"}