--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sat Apr 16 15:47:52 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sat Apr 16 16:15:37 2011 +0200
@@ -65,7 +65,7 @@
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