# HG changeset patch
# User berghofe
# Date 1265817940 -3600
# Node ID 7722bcb5c37c799bf486466ce5060a7b81f8c8e2
# Parent  4554bb2abfa3871cde6c6bac9278376d2619a3b2# Parent  45dec8e27c4b935967f8809f97cffefbc057bd4d
merged

diff -r 4554bb2abfa3 -r 7722bcb5c37c src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Wed Feb 10 15:52:12 2010 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Feb 10 17:05:40 2010 +0100
@@ -303,8 +303,10 @@
       HOLogic.dest_eq |> fst |> strip_comb |> snd |> take_prefix is_Var |> fst;
     val (pvars, ctxtvars) = List.partition
       (equal HOLogic.boolT o body_type o snd)
-      (subtract (op =) (map dest_Var fvars) (fold_rev Term.add_vars (map Logic.strip_assums_concl
-        (prems_of (hd rec_rewrites))) []));
+      (subtract (op =)
+        (Term.add_vars (concl_of (hd rec_rewrites)) [])
+        (fold_rev (Term.add_vars o Logic.strip_assums_concl)
+           (prems_of (hd rec_rewrites)) []));
     val cfs = defs' |> hd |> snd |> strip_comb |> snd |>
       curry (List.take o swap) (length fvars) |> map cert;
     val invs' = (case invs of