src/HOL/Tools/Quickcheck/random_generators.ML
changeset 54742 7a86358a3c0b
parent 51717 9e7d1c139569
child 55414 eab03e9cee8a
     1.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -107,7 +107,7 @@
     1.4      fun tac ctxt =
     1.5        ALLGOALS (rtac rule)
     1.6        THEN ALLGOALS (simp_tac (put_simpset rew_ss ctxt))
     1.7 -      THEN (ALLGOALS (Proof_Context.fact_tac eqs2))
     1.8 +      THEN (ALLGOALS (Proof_Context.fact_tac ctxt eqs2))
     1.9      val simp = Goal.prove_sorry lthy' [v] [] eq (tac o #context);
    1.10    in (simp, lthy') end;
    1.11  
    1.12 @@ -166,7 +166,7 @@
    1.13      fun prove_simps proto_simps lthy =
    1.14        let
    1.15          val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
    1.16 -        val tac = ALLGOALS (Proof_Context.fact_tac ext_simps);
    1.17 +        val tac = ALLGOALS (Proof_Context.fact_tac lthy ext_simps);
    1.18        in (map (fn prop => Goal.prove_sorry lthy vs [] prop (K tac)) eqs, lthy) end;
    1.19      val b = Binding.conceal (Binding.qualify true prfx
    1.20        (Binding.qualify true name (Binding.name "simps")));