# HG changeset patch
# User bulwahn
# Date 1327656690 -3600
# Node ID 6d9535e5291540d0618a64c189b684be4789b6e0
# Parent  c59b8560eb48b33e0fbf598536004d327cc9a348
adding some basic handling that unfolds a conjecture in a locale before testing it with quickcheck

diff -r c59b8560eb48 -r 6d9535e52915 src/Tools/quickcheck.ML
--- 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