tuned;

--- a/src/Pure/consts.ML	Thu Dec 07 17:58:42 2006 +0100
+++ b/src/Pure/consts.ML	Thu Dec 07 17:58:44 2006 +0100
@@ -145,7 +145,8 @@
     fun cert tm =
       let
         val (head, args) = Term.strip_comb tm;
-        fun comb h = Term.list_comb (h, map cert args);
+        val args' = map cert args;
+        fun comb head' = Term.list_comb (head', args');
       in
         (case head of
           Abs (x, T, t) => comb (Abs (x, T, cert t))
@@ -160,7 +161,7 @@
                 (case (kind, expand_abbrevs) of
                   (Abbreviation u, true) =>
                     Term.betapplys (Envir.expand_atom T' (U, u) handle TYPE _ =>
-                      err "Illegal type for abbreviation" (c, T), map cert args)
+                      err "Illegal type for abbreviation" (c, T), args')
                 | _ => comb head)
             end
         | _ => comb head)