--- a/src/HOL/Product_Type.thy Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Product_Type.thy Fri Mar 21 20:33:56 2014 +0100
@@ -457,7 +457,7 @@
ML {*
(* replace parameters of product type by individual component parameters *)
local (* filtering with exists_paired_all is an essential optimization *)
- fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) =
+ fun exists_paired_all (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) =
can HOLogic.dest_prodT T orelse exists_paired_all t
| exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u
| exists_paired_all (Abs (_, _, t)) = exists_paired_all t