--- a/src/Tools/Code/code_printer.ML Tue Sep 20 01:32:04 2011 +0200
+++ b/src/Tools/Code/code_printer.ML Tue Sep 20 09:30:19 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, ((_, (arg_tys, _)), _)), ts)) =
case const_syntax c of
NONE => brackify fxy (print_app_expr some_thm vars app)
| SOME (Plain_const_syntax (_, s)) =>
@@ -323,7 +323,7 @@
| SOME (Complex_const_syntax (k, print)) =>
let
fun print' fxy ts =
- print (print_term some_thm) some_thm vars fxy (ts ~~ take k function_typs);
+ print (print_term some_thm) some_thm vars fxy (ts ~~ take k arg_tys);
in
if k = length ts
then print' fxy ts