--- a/src/HOL/Nominal/nominal_primrec.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Wed Oct 21 10:15:31 2009 +0200
@@ -305,8 +305,8 @@
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)
- (fold_rev Term.add_vars (map Logic.strip_assums_concl
- (prems_of (hd rec_rewrites))) [] \\ map dest_Var fvars);
+ (subtract (op =) (map dest_Var fvars) (fold_rev Term.add_vars (map 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