changeset 33955 | fff6f11b1f09 |
parent 32924 | d2e9b2dab760 |
child 33957 | e9afca2118d4 |
--- a/src/Tools/Code/code_printer.ML Tue Nov 24 14:37:23 2009 +0100 +++ b/src/Tools/Code/code_printer.ML Tue Nov 24 17:28:25 2009 +0100 @@ -231,7 +231,7 @@ of NONE => brackify fxy (pr_app thm vars app) | SOME (k, pr) => let - fun pr' fxy ts = pr (pr_term thm) thm vars fxy (ts ~~ curry Library.take k tys); + fun pr' fxy ts = pr (pr_term thm) thm vars fxy (ts ~~ curry (uncurry take) k tys); in if k = length ts then pr' fxy ts else if k < length ts