src/Tools/Code/code_ml.ML
changeset 44789 5a062c23c7db
parent 44788 8b935f1b3cf8
child 45009 99e1965f9c21
     1.1 --- a/src/Tools/Code/code_ml.ML	Wed Sep 07 13:51:30 2011 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Wed Sep 07 13:51:32 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