--- 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)