--- a/src/Tools/Code/code_ml.ML Wed Sep 07 13:51:30 2011 +0200
+++ b/src/Tools/Code/code_ml.ML Wed Sep 07 13:51:32 2011 +0200
@@ -117,7 +117,7 @@
then print_case is_pseudo_fun some_thm vars fxy cases
else print_app is_pseudo_fun some_thm vars fxy c_ts
| NONE => print_case is_pseudo_fun some_thm vars fxy cases)
- and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), function_typs), _)), ts)) =
+ and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (function_typs, _)), _)), ts)) =
if is_cons c then
let val k = length function_typs in
if k < 2 orelse length ts = k
@@ -417,7 +417,7 @@
then print_case is_pseudo_fun some_thm vars fxy cases
else print_app is_pseudo_fun some_thm vars fxy c_ts
| NONE => print_case is_pseudo_fun some_thm vars fxy cases)
- and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), tys), _)), ts)) =
+ and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (tys, _)), _)), ts)) =
if is_cons c then
let val k = length tys in
if length ts = k