src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 59498 50b60f501b05
parent 59434 94194354e004
child 59621 291934bac95e
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Feb 10 14:29:36 2015 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Feb 10 14:48:26 2015 +0100
     1.3 @@ -54,7 +54,7 @@
     1.4      |> `(fn lthy => Syntax.check_term lthy eq)
     1.5      |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
     1.6      |> snd
     1.7 -    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
     1.8 +    |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
     1.9    end;
    1.10  
    1.11  fun ensure_partial_term_of (tyco, (raw_vs, _)) thy =
    1.12 @@ -187,7 +187,7 @@
    1.13        |> Quickcheck_Common.define_functions
    1.14          (fn narrowings => mk_equations descr vs narrowings, NONE)
    1.15          prfx [] narrowingsN (map narrowingT (Ts @ Us))
    1.16 -      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    1.17 +      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
    1.18      else
    1.19        thy
    1.20    end;