--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Nov 19 08:25:54 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Nov 19 08:25:57 2009 +0100
@@ -83,7 +83,7 @@
val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac
val _ = tracing (Display.string_of_thm ctxt' intro)
val thy'' = thy'
- |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro)
+ |> Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro)
|> Predicate_Compile.preprocess options full_constname
|> Predicate_Compile_Core.add_equations options [full_constname]
(* |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*)