src/HOL/Nominal/nominal_primrec.ML
changeset 29276 94b1ffec9201
parent 29265 5b4247055bd7
child 29581 b3b33e0298eb
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Wed Dec 31 18:53:19 2008 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Dec 31 19:54:03 2008 +0100
     1.3 @@ -155,7 +155,7 @@
     1.4                val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
     1.5                val rargs = map fst recs;
     1.6                val subs = map (rpair dummyT o fst)
     1.7 -                (rev (rename_wrt_term rhs rargs));
     1.8 +                (rev (Term.rename_wrt_term rhs rargs));
     1.9                val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
    1.10                  (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
    1.11                    handle RecError s => primrec_eq_err lthy s eq