diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML	Fri Mar 21 20:33:56 2014 +0100
@@ -40,7 +40,7 @@
 
 
 (* Removes all quantifiers from a term, replacing bound variables by frees. *)
-fun dest_all_all (t as (Const ("all",_) $ _)) =
+fun dest_all_all (t as (Const (@{const_name Pure.all},_) $ _)) =
   let
     val (v,b) = Logic.dest_all t |> apfst Free
     val (vs, b') = dest_all_all b