src/HOL/Tools/Quickcheck/quickcheck_common.ML

       #> apfst fst) (names ~~ Ts)
     #> (fn (consts, lthy) =>
       let
         val eqs_t = mk_equations consts
         val eqs = map (fn eq => Goal.prove lthy argnames [] eq
-          (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
+          (fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of lthy))) eqs_t
       in
         fold (fn (name, eq) => Local_Theory.note
         ((Binding.conceal (Binding.qualify true prfx
            (Binding.qualify true name (Binding.name "simps"))),
            Code.add_default_eqn_attrib :: map (Attrib.internal o K)