src/Tools/quickcheck.ML
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;