--- a/src/HOL/Nominal/nominal_primrec.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Fri Mar 21 20:33:56 2014 +0100
@@ -32,8 +32,8 @@
fun unquantify t =
let
- val (vs, Ts) = split_list (strip_qnt_vars "all" t);
- val body = strip_qnt_body "all" t;
+ val (vs, Ts) = split_list (strip_qnt_vars @{const_name Pure.all} t);
+ val body = strip_qnt_body @{const_name Pure.all} t;
val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms
(fn Free (v, _) => insert (op =) v | _ => I) body []))
in (curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body) end;