changeset 59582 | 0fbed69ff081 |
parent 59439 | 397ce0940c44 |
child 59936 | b8ffc3dc9e24 |
--- a/src/Tools/quickcheck.ML Tue Mar 03 19:08:04 2015 +0100 +++ b/src/Tools/quickcheck.ML Wed Mar 04 19:53:18 2015 +0100 @@ -344,7 +344,7 @@ 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 (gi, frees) = Logic.goal_params (Thm.prop_of st) i; val some_locale = Named_Target.bottom_locale_of lthy; val assms = if Config.get lthy no_assms then []