# HG changeset patch
# User berghofe
# Date 1265817918 -3600
# Node ID 45dec8e27c4b935967f8809f97cffefbc057bd4d
# Parent  17b7940f43e48e53063d2c96d52eea8687217a0e
Fixed bug in code for guessing the name of the variable representing the freshness context.

diff -r 17b7940f43e4 -r 45dec8e27c4b src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Wed Feb 10 12:04:57 2010 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Feb 10 17:05:18 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