src/Tools/Code/code_printer.ML
changeset 48072 ace701efe203
parent 47576 b32aae03e3d6
child 50618 36850cf745e7
     1.1 --- a/src/Tools/Code/code_printer.ML	Mon Jun 04 12:55:54 2012 +0200
     1.2 +++ b/src/Tools/Code/code_printer.ML	Tue Jun 05 07:05:56 2012 +0200
     1.3 @@ -315,7 +315,7 @@
     1.4        |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
     1.5  
     1.6  fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
     1.7 -    (app as ((c, ((_, (arg_tys, _)), _)), ts)) =
     1.8 +    (app as ({ name = c, dom, ... }, ts)) =
     1.9    case const_syntax c of
    1.10      NONE => brackify fxy (print_app_expr some_thm vars app)
    1.11    | SOME (Plain_const_syntax (_, s)) =>
    1.12 @@ -323,7 +323,7 @@
    1.13    | SOME (Complex_const_syntax (k, print)) =>
    1.14        let
    1.15          fun print' fxy ts =
    1.16 -          print (print_term some_thm) some_thm vars fxy (ts ~~ take k arg_tys);
    1.17 +          print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
    1.18        in
    1.19          if k = length ts
    1.20          then print' fxy ts