diff -r b33b42211bbf -r 188826f1ccdb Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/nominal_library.ML	Mon Mar 24 15:31:17 2014 +0000
@@ -298,7 +298,8 @@
 (* decompses a formula into params, premises and a conclusion *)
 fun strip_full_horn trm =
   let
-    fun strip_outer_params (Const ("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T)
+    fun strip_outer_params (Const (@{const_name Pure.all}, _) $ Abs (a, T, t)) = 
+      strip_outer_params t |>> cons (a, T)
     | strip_outer_params B = ([], B)
 
     val (params, body) = strip_outer_params trm