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