# HG changeset patch
# User wenzelm
# Date 1460642542 -7200
# Node ID 4b71cd0bfe142423d7eaabeb674ff697c5cdf9a2
# Parent  3a01f1f58630a98a9cc75c6acde7030c75048c18
tuned;

diff -r 3a01f1f58630 -r 4b71cd0bfe14 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Thu Apr 14 15:56:30 2016 +0200
+++ b/src/Tools/quickcheck.ML	Thu Apr 14 16:02:22 2016 +0200
@@ -338,27 +338,28 @@
 
 fun test_goal (time_limit, is_interactive) (insts, eval_terms) i state =
   let
-    val lthy = Proof.context_of state;
+    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 some_locale = Named_Target.bottom_locale_of lthy;
+    val opt_locale = Named_Target.bottom_locale_of ctxt;
     val assms =
-      if Config.get lthy no_assms then []
+      if Config.get ctxt no_assms then []
       else
-        (case some_locale of
-          NONE => Assumption.all_assms_of lthy
-        | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy));
+        (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 lthy t));
-    val config = locale_config_of (Config.get lthy locale);
+      | SOME t => the_default [] (all_axioms_of ctxt t));
+    val config = locale_config_of (Config.get ctxt locale);
     val goals =
-      (case some_locale of
+      (case opt_locale of
         NONE => [(proto_goal, eval_terms)]
       | SOME locale =>
           fold (fn c =>
@@ -370,11 +371,11 @@
                 (Locale.registrations_of (Context.Theory thy) (* FIXME !? *) locale))
             else I) config []);
     val _ =
-      verbose_message lthy
+      verbose_message ctxt
         (Pretty.string_of
-          (Pretty.big_list ("Checking goals: ") (map (Syntax.pretty_term lthy o fst) goals)));
+          (Pretty.big_list ("Checking goals: ") (map (Syntax.pretty_term ctxt o fst) goals)));
   in
-    test_terms lthy (time_limit, is_interactive) insts goals
+    test_terms ctxt (time_limit, is_interactive) insts goals
   end;