src/Tools/Code/code_ml.ML
changeset 44788 8b935f1b3cf8
parent 43345 165188299a25
child 44789 5a062c23c7db
     1.1 --- a/src/Tools/Code/code_ml.ML	Wed Sep 07 11:36:39 2011 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Wed Sep 07 13:51:30 2011 +0200
     1.3 @@ -117,7 +117,7 @@
     1.4                  then print_case is_pseudo_fun some_thm vars fxy cases
     1.5                  else print_app is_pseudo_fun some_thm vars fxy c_ts
     1.6              | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
     1.7 -    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), function_typs)), ts)) =
     1.8 +    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), function_typs), _)), ts)) =
     1.9        if is_cons c then
    1.10          let val k = length function_typs in
    1.11            if k < 2 orelse length ts = k
    1.12 @@ -417,7 +417,7 @@
    1.13                  then print_case is_pseudo_fun some_thm vars fxy cases
    1.14                  else print_app is_pseudo_fun some_thm vars fxy c_ts
    1.15              | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
    1.16 -    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =
    1.17 +    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), tys), _)), ts)) =
    1.18        if is_cons c then
    1.19          let val k = length tys in
    1.20            if length ts = k