--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Tue Jan 22 13:32:41 2013 +0100
@@ -292,8 +292,9 @@
val bound_vars' = union (op =) (vars_of lhs) (union (op =) varnames bound_vars)
val cont_t = mk_smart_test_term' concl bound_vars' (new_assms @ assms) genuine
in
- mk_test (vars_of lhs, Datatype_Case.make_case ctxt Datatype_Case.Quiet [] lhs
- [(list_comb (constr, vars), cont_t), (dummy_var, none_t)])
+ mk_test (vars_of lhs,
+ Datatype_Case.make_case ctxt Datatype_Case.Quiet Name.context lhs
+ [(list_comb (constr, vars), cont_t), (dummy_var, none_t)])
end
else c (assm, assms)
fun default (assm, assms) =