changeset 32859 | 204f749f35a9 |
parent 32740 | 9dd0a2f83429 |
child 32966 | 5b21661fe618 |
--- a/src/Tools/quickcheck.ML Fri Oct 02 21:42:31 2009 +0200 +++ b/src/Tools/quickcheck.ML Fri Oct 02 22:02:11 2009 +0200 @@ -143,7 +143,7 @@ val thy = Proof.theory_of state; fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t | strip t = t; - val (_, (_, st)) = Proof.get_goal state; + val (_, st) = Proof.flat_goal state; val (gi, frees) = Logic.goal_params (prop_of st) i; val gi' = Logic.list_implies (assms, subst_bounds (frees, strip gi)) |> monomorphic_term thy insts default_T