src/HOL/Tools/quickcheck_generators.ML

       |> Drule.instantiate ([(aT, icT)],
            [(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)]);
     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;
 
 fun random_aux_primrec_multi auxname [eq] lthy =

             val proj_simps = map (snd o snd) proj_defs;
             fun tac { context = ctxt, prems = _ } =
               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'
         ||>> fold_map (LocalTheory.define Thm.definitionK) proj_defs
         |-> (fn (aux_simp, proj_defs) => prove_eqs aux_simp proj_defs)

     val proto_eqs = map mk_proto_eq eqs;
     fun prove_simps proto_simps lthy =
       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
     |> random_aux_primrec_multi (name ^ prfx) proto_eqs
     |-> (fn proto_simps => prove_simps proto_simps)