src/HOL/Tools/Quickcheck/random_generators.ML
changeset 51551 88d1d19fb74f
parent 51143 0a2371e7ced3
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Mar 27 14:08:03 2013 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Mar 27 14:19:18 2013 +0100
     1.3 @@ -107,7 +107,7 @@
     1.4      val tac = ALLGOALS (rtac rule)
     1.5        THEN ALLGOALS (simp_tac rew_ss)
     1.6        THEN (ALLGOALS (Proof_Context.fact_tac eqs2))
     1.7 -    val simp = Skip_Proof.prove lthy' [v] [] eq (K tac);
     1.8 +    val simp = Goal.prove_sorry lthy' [v] [] eq (K tac);
     1.9    in (simp, lthy') end;
    1.10  
    1.11  end;
    1.12 @@ -144,7 +144,7 @@
    1.13                ALLGOALS (simp_tac (HOL_ss addsimps proj_simps))
    1.14                THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp])
    1.15                THEN ALLGOALS (simp_tac (HOL_ss addsimps [@{thm fst_conv}, @{thm snd_conv}]));
    1.16 -          in (map (fn prop => Skip_Proof.prove lthy [v] [] prop tac) eqs, lthy) end;
    1.17 +          in (map (fn prop => Goal.prove_sorry lthy [v] [] prop tac) eqs, lthy) end;
    1.18        in
    1.19          lthy
    1.20          |> random_aux_primrec aux_eq'
    1.21 @@ -165,7 +165,7 @@
    1.22        let
    1.23          val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
    1.24          val tac = ALLGOALS (Proof_Context.fact_tac ext_simps);
    1.25 -      in (map (fn prop => Skip_Proof.prove lthy vs [] prop (K tac)) eqs, lthy) end;
    1.26 +      in (map (fn prop => Goal.prove_sorry lthy vs [] prop (K tac)) eqs, lthy) end;
    1.27      val b = Binding.conceal (Binding.qualify true prfx
    1.28        (Binding.qualify true name (Binding.name "simps")));
    1.29    in