src/Tools/quickcheck.ML
changeset 56245 84fc7dfa3cd4
parent 55630 47286c847749
child 56467 8d7d6f17c6a7
     1.1 --- a/src/Tools/quickcheck.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/Tools/quickcheck.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -358,7 +358,7 @@
     1.4      val lthy = Proof.context_of state;
     1.5      val thy = Proof.theory_of state;
     1.6      val _ = message lthy "Quickchecking..."
     1.7 -    fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
     1.8 +    fun strip (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = strip t
     1.9        | strip t = t;
    1.10      val {goal = st, ...} = Proof.raw_goal state;
    1.11      val (gi, frees) = Logic.goal_params (prop_of st) i;