# HG changeset patch
# User berghofe
# Date 1173540715 -3600
# Node ID 081a6285231340dd769f8a3f2ba6b48e2821984e
# Parent  400fa18e951f76f80e19e1a79f339772beac81d6
- Replaced fold by fold_rev to make sure that list of predicate
  variables pvars (for invariants) is in the correct order
- Adapted to new format of datatype descriptor

diff -r 400fa18e951f -r 081a62852313 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Sat Mar 10 16:28:06 2007 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sat Mar 10 16:31:55 2007 +0100
@@ -255,6 +255,9 @@
       if null dts then
         primrec_err ("datatypes " ^ commas_quote tnames ^ "\nare not mutually recursive")
       else snd (hd dts);
+    val descr = map (fn (i, (tname, args, constrs)) => (i, (tname, args,
+      map (fn (cname, cargs) => (cname, fold (fn (dTs, dT) => fn dTs' =>
+        dTs' @ dTs @ [dT]) cargs [])) constrs))) descr;
     val (fnameTs, fnss) =
       fold_rev (process_fun thy descr rec_eqns) main_fns ([], []);
     val (fs, defs) = fold_rev (get_fns fnss) (descr ~~ rec_names) ([], []);
@@ -289,7 +292,7 @@
       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 Term.add_vars (map Logic.strip_assums_concl
+      (fold_rev Term.add_vars (map Logic.strip_assums_concl
         (prems_of (hd rec_rewrites))) [] \\ map dest_Var fvars);
     val cfs = defs' |> hd |> snd |> strip_comb |> snd |>
       curry (List.take o swap) (length fvars) |> map cert;