src/Tools/quickcheck.ML

     val _ = message lthy "Quickchecking..."
     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 (prop_of st) i;
-    val some_locale =
-      (case (Option.map #target o Named_Target.peek) lthy of
-        NONE => NONE
-      | SOME "" => NONE
-      | SOME locale => SOME locale);
+    val some_locale = Named_Target.locale_of lthy;
     val assms =
       if Config.get lthy no_assms then []
       else
         (case some_locale of
           NONE => Assumption.all_assms_of lthy