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.
merged
authorberghofe
Wed, 10 Feb 2010 17:05:40 +0100
changeset 35099 7722bcb5c37c
parent 35097 4554bb2abfa3 (current diff)
parent 35098 45dec8e27c4b (diff)
child 35100 53754ec7360b
merged
--- 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
isabelle