--- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Sat Oct 24 16:55:42 2009 +0200
@@ -65,7 +65,7 @@
|> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro)
|> Predicate_Compile.preprocess Predicate_Compile_Aux.default_options full_constname
|> Predicate_Compile_Core.add_equations Predicate_Compile_Aux.default_options [full_constname]
- |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]
+ (* |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*)
|> Predicate_Compile_Core.add_quickcheck_equations Predicate_Compile_Aux.default_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