--- 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
@@ -63,10 +63,10 @@
val _ = tracing (Display.string_of_thm ctxt' intro)
val thy'' = thy'
|> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro)
- |> Predicate_Compile.preprocess full_constname
- |> Predicate_Compile_Core.add_equations NONE [full_constname]
- |> Predicate_Compile_Core.add_sizelim_equations NONE [full_constname]
- |> Predicate_Compile_Core.add_quickcheck_equations NONE [full_constname]
+ |> Predicate_Compile.preprocess Predicate_Compile_Aux.default_options full_constname
+ |> Predicate_Compile_Core.add_equations Predicate_Compile_Aux.default_options NONE [full_constname]
+ |> Predicate_Compile_Core.add_sizelim_equations Predicate_Compile_Aux.default_options NONE [full_constname]
+ |> Predicate_Compile_Core.add_quickcheck_equations Predicate_Compile_Aux.default_options NONE [full_constname]
val sizelim_modes = Predicate_Compile_Core.sizelim_modes_of thy'' full_constname
val modes = Predicate_Compile_Core.generator_modes_of thy'' full_constname
val prog =