src/Tools/Code/code_ml.ML
changeset 44788 8b935f1b3cf8
parent 43345 165188299a25
child 44789 5a062c23c7db
--- a/src/Tools/Code/code_ml.ML	Wed Sep 07 11:36:39 2011 +0200
+++ b/src/Tools/Code/code_ml.ML	Wed Sep 07 13:51:30 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