--- a/src/Tools/quickcheck.ML Fri Jun 06 19:19:46 2014 +0200
+++ b/src/Tools/quickcheck.ML Sat Jun 07 08:16:03 2014 +0200
@@ -362,11 +362,7 @@
| 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