src/HOL/Tools/Quickcheck/random_generators.ML

--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Tue Feb 10 14:48:26 2015 +0100
@@ -263,7 +263,7 @@
           Specification.definition (NONE, (apfst Binding.conceal
             Attrib.empty_binding, random_def))) random_defs')
     |> snd
-    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
+    |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   end;