Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixed bug in code for guessing the name of the variable representing the freshness context.
authorberghofe
Wed, 10 Feb 2010 17:05:18 +0100
changeset 35098 45dec8e27c4b
parent 35089 17b7940f43e4
child 35099 7722bcb5c37c
Fixed bug in code for guessing the name of the variable representing the freshness context.
src/HOL/Nominal/nominal_primrec.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle