--- a/src/Tools/quickcheck.ML Fri Jan 27 10:19:55 2012 +0100
+++ b/src/Tools/quickcheck.ML Fri Jan 27 10:31:30 2012 +0100
@@ -324,10 +324,20 @@
of NONE => Assumption.all_assms_of lthy
| SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy);
val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
+ fun assms_of locale = case fst (Locale.intros_of thy locale) of NONE => []
+ | SOME th =>
+ let
+ val t = the_single (Assumption.all_assms_of (Locale.init locale thy))
+ val (tyenv, tenv) =
+ Pattern.match thy (concl_of th, term_of t) (Vartab.empty, Vartab.empty)
+ in
+ map (Envir.subst_term (tyenv, tenv)) (prems_of th)
+ end
val goals = case some_locale
of NONE => [(proto_goal, eval_terms)]
| SOME locale =>
- map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
+ (Logic.list_implies (assms_of locale, proto_goal), eval_terms) ::
+ map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
(Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
in
test_terms lthy (time_limit, is_interactive) insts goals