src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML

 structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK =
 struct
 
 val test_ref =
   Unsynchronized.ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option)
+
 val target = "Quickcheck"
 
 fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs
 val mk_predT = #mk_predT (dest_compfuns Predicate_Compile_Core.pred_compfuns)
 val mk_rpredT = #mk_predT (dest_compfuns Predicate_Compile_Core.rpred_compfuns)

     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)
       |> 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_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]
+      (* |> 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  
     val prog =
       if member (op =) modes ([], []) then
         let