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