# 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>\Pure.all\, _) $ 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;