changeset 56245 | 84fc7dfa3cd4 |
parent 55630 | 47286c847749 |
child 56467 | 8d7d6f17c6a7 |
--- a/src/Tools/quickcheck.ML Fri Mar 21 15:12:03 2014 +0100 +++ b/src/Tools/quickcheck.ML Fri Mar 21 20:33:56 2014 +0100 @@ -358,7 +358,7 @@ val lthy = Proof.context_of state; val thy = Proof.theory_of state; val _ = message lthy "Quickchecking..." - fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t + 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;