diff -r 8b935f1b3cf8 -r 5a062c23c7db src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Wed Sep 07 13:51:30 2011 +0200
+++ b/src/Tools/Code/code_printer.ML	Wed Sep 07 13:51:32 2011 +0200
@@ -315,7 +315,7 @@
       |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
 
 fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
-    (app as ((c, ((_, function_typs), _)), ts)) =
+    (app as ((c, ((_, (function_typs, _)), _)), ts)) =
   case const_syntax c of
     NONE => brackify fxy (print_app_expr some_thm vars app)
   | SOME (Plain_const_syntax (_, s)) =>