# HG changeset patch
# User bulwahn
# Date 1257491915 -3600
# Node ID e1552d8718accfd4fd77404d07fad4065dbde247
# Parent  0df4f6e46e5e789264eb3d9397e006e388cd0674
adopted the predicate compile quickcheck

diff -r 0df4f6e46e5e -r e1552d8718ac src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Nov 06 08:18:35 2009 +0100
@@ -87,11 +87,11 @@
       (*  |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*)
       |> Predicate_Compile_Core.add_quickcheck_equations options [full_constname]
     val depth_limited_modes = Predicate_Compile_Core.depth_limited_modes_of thy'' full_constname
-    val modes = Predicate_Compile_Core.generator_modes_of thy'' full_constname  
+    val modes = Predicate_Compile_Core.random_modes_of thy'' full_constname  
     val prog =
       if member (op =) modes ([], []) then
         let
-          val name = Predicate_Compile_Core.generator_name_of thy'' full_constname ([], [])
+          val name = Predicate_Compile_Core.random_function_name_of thy'' full_constname ([], [])
           val T = [@{typ code_numeral}] ---> (mk_randompredT (HOLogic.mk_tupleT (map snd vs')))
           in Const (name, T) $ Bound 0 end
       (*else if member (op =) depth_limited_modes ([], []) then