# HG changeset patch
# User haftmann
# Date 1618515943 0
# Node ID ed5226fdf89d32e5d537e2d4e22d9bfb13c040a6
# Parent  dabe295c3f62b2ba2f1df67704c1566d34b2092d
proper context variable handling when stripping leadings quantifiers from test goals

diff -r dabe295c3f62 -r ed5226fdf89d src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Wed Apr 14 21:15:24 2021 +0200
+++ b/src/Tools/quickcheck.ML	Thu Apr 15 19:45:43 2021 +0000
@@ -342,24 +342,22 @@
   let
     val ctxt = Proof.context_of state;
     val thy = Proof.theory_of state;
-
-    fun strip (Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, _, t)) = strip t
-      | strip t = t;
-    val {goal = st, ...} = Proof.raw_goal state;
-    val (gi, frees) = Logic.goal_params (Thm.prop_of st) i;
     val opt_locale = Named_Target.bottom_locale_of ctxt;
+    fun axioms_of locale =
+      (case fst (Locale.specification_of thy locale) of
+        NONE => []
+      | SOME t => the_default [] (all_axioms_of ctxt t));
+    val config = locale_config_of (Config.get ctxt locale);
     val assms =
       if Config.get ctxt no_assms then []
       else
         (case opt_locale of
           NONE => Assumption.all_assms_of ctxt
         | SOME locale => Assumption.local_assms_of ctxt (Locale.init locale thy));
-    val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
-    fun axioms_of locale =
-      (case fst (Locale.specification_of thy locale) of
-        NONE => []
-      | SOME t => the_default [] (all_axioms_of ctxt t));
-    val config = locale_config_of (Config.get ctxt locale);
+    val {goal = st, ...} = Proof.raw_goal state;
+    val (gi, _) = Logic.goal_params (Thm.prop_of st) i;
+    val ((_, raw_goal), ctxt') = Variable.focus NONE gi ctxt;
+    val proto_goal = Logic.list_implies (map Thm.term_of assms, raw_goal);
     val goals =
       (case opt_locale of
         NONE => [(proto_goal, eval_terms)]
@@ -373,11 +371,11 @@
                 (Locale.registrations_of (Context.Theory thy) (* FIXME !? *) locale))
             else I) config []);
     val _ =
-      verbose_message ctxt
+      verbose_message ctxt'
         (Pretty.string_of
-          (Pretty.big_list ("Checking goals: ") (map (Syntax.pretty_term ctxt o fst) goals)));
+          (Pretty.big_list ("Checking goals: ") (map (Syntax.pretty_term ctxt' o fst) goals)));
   in
-    test_terms ctxt (time_limit, is_interactive) insts goals
+    test_terms ctxt' (time_limit, is_interactive) insts goals
   end;