tuned;
authorwenzelm
Thu Dec 07 17:58:44 2006 +0100 (2006-12-07 ago)
changeset 216949f65fecb6e10
parent 21693 44cc5b3bb5bf
child 21695 6c07cc87fe2b
tuned;
src/Pure/consts.ML
     1.1 --- a/src/Pure/consts.ML	Thu Dec 07 17:58:42 2006 +0100
     1.2 +++ b/src/Pure/consts.ML	Thu Dec 07 17:58:44 2006 +0100
     1.3 @@ -145,7 +145,8 @@
     1.4      fun cert tm =
     1.5        let
     1.6          val (head, args) = Term.strip_comb tm;
     1.7 -        fun comb h = Term.list_comb (h, map cert args);
     1.8 +        val args' = map cert args;
     1.9 +        fun comb head' = Term.list_comb (head', args');
    1.10        in
    1.11          (case head of
    1.12            Abs (x, T, t) => comb (Abs (x, T, cert t))
    1.13 @@ -160,7 +161,7 @@
    1.14                  (case (kind, expand_abbrevs) of
    1.15                    (Abbreviation u, true) =>
    1.16                      Term.betapplys (Envir.expand_atom T' (U, u) handle TYPE _ =>
    1.17 -                      err "Illegal type for abbreviation" (c, T), map cert args)
    1.18 +                      err "Illegal type for abbreviation" (c, T), args')
    1.19                  | _ => comb head)
    1.20              end
    1.21          | _ => comb head)