diff -r 8b74cfea913a -r 99e1965f9c21 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Tue Sep 20 01:32:04 2011 +0200
+++ b/src/Tools/Code/code_ml.ML	Tue Sep 20 09:30:19 2011 +0200
@@ -117,9 +117,9 @@
                 then print_case is_pseudo_fun some_thm vars fxy cases
                 else print_app is_pseudo_fun some_thm vars fxy c_ts
             | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
-    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (function_typs, _)), _)), ts)) =
+    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (arg_tys, _)), _)), ts)) =
       if is_cons c then
-        let val k = length function_typs in
+        let val k = length arg_tys in
           if k < 2 orelse length ts = k
           then (str o deresolve) c
             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)