diff -r 15489e162b21 -r fbd2bb2489a8 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -149,7 +149,7 @@
     val tac = ALLGOALS (rtac rule)
       THEN ALLGOALS (simp_tac rew_ss)
       THEN (ALLGOALS (ProofContext.fact_tac (flat eqs2)))
-    val simp = SkipProof.prove lthy' [v] [] eq (K tac);
+    val simp = Skip_Proof.prove lthy' [v] [] eq (K tac);
   in (simp, lthy') end;
 
 end;
@@ -185,7 +185,7 @@
               ALLGOALS (simp_tac (HOL_ss addsimps proj_simps))
               THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp])
               THEN ALLGOALS (simp_tac (HOL_ss addsimps [fst_conv, snd_conv]));
-          in (map (fn prop => SkipProof.prove lthy [v] [] prop tac) eqs, lthy) end;
+          in (map (fn prop => Skip_Proof.prove lthy [v] [] prop tac) eqs, lthy) end;
       in
         lthy
         |> random_aux_primrec aux_eq'
@@ -206,7 +206,7 @@
       let
         val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
         val tac = ALLGOALS (ProofContext.fact_tac ext_simps);
-      in (map (fn prop => SkipProof.prove lthy vs [] prop (K tac)) eqs, lthy) end;
+      in (map (fn prop => Skip_Proof.prove lthy vs [] prop (K tac)) eqs, lthy) end;
     val b = Binding.qualify true prfx (Binding.qualify true name (Binding.name "simps"));
   in
     lthy