--- 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