--- a/src/HOL/Nominal/nominal_inductive2.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Thu Aug 19 16:08:59 2010 +0200
@@ -82,7 +82,7 @@
| split_conj _ _ _ _ = NONE;
fun strip_all [] t = t
- | strip_all (_ :: xs) (Const (@{const_name "All"}, _) $ Abs (s, T, t)) = strip_all xs t;
+ | strip_all (_ :: xs) (Const (@{const_name All}, _) $ Abs (s, T, t)) = strip_all xs t;
(*********************************************************************)
(* maps R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t)) *)