equal
deleted
inserted
replaced
360 val _ = message lthy "Quickchecking..." |
360 val _ = message lthy "Quickchecking..." |
361 fun strip (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = strip t |
361 fun strip (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = strip t |
362 | strip t = t; |
362 | strip t = t; |
363 val {goal = st, ...} = Proof.raw_goal state; |
363 val {goal = st, ...} = Proof.raw_goal state; |
364 val (gi, frees) = Logic.goal_params (prop_of st) i; |
364 val (gi, frees) = Logic.goal_params (prop_of st) i; |
365 val some_locale = Named_Target.locale_of lthy; |
365 val some_locale = Named_Target.bottom_locale_of lthy; |
366 val assms = |
366 val assms = |
367 if Config.get lthy no_assms then [] |
367 if Config.get lthy no_assms then [] |
368 else |
368 else |
369 (case some_locale of |
369 (case some_locale of |
370 NONE => Assumption.all_assms_of lthy |
370 NONE => Assumption.all_assms_of lthy |