--- a/src/HOL/Tools/old_primrec.ML Thu Oct 29 23:48:56 2009 +0100
+++ b/src/HOL/Tools/old_primrec.ML Thu Oct 29 23:49:55 2009 +0100
@@ -34,11 +34,11 @@
same type in all introduction rules*)
fun unify_consts thy cs intr_ts =
(let
- fun varify (t, (i, ts)) =
+ fun varify t (i, ts) =
let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify [] t))
in (maxidx_of_term t', t'::ts) end;
- val (i, cs') = List.foldr varify (~1, []) cs;
- val (i', intr_ts') = List.foldr varify (i, []) intr_ts;
+ val (i, cs') = fold_rev varify cs (~1, []);
+ val (i', intr_ts') = fold_rev varify intr_ts (i, []);
val rec_consts = fold Term.add_consts cs' [];
val intr_consts = fold Term.add_consts intr_ts' [];
fun unify (cname, cT) =