src/Pure/Syntax/syntax.ML
changeset 33957 e9afca2118d4
parent 33955 fff6f11b1f09
child 35111 18cd034922ba
--- a/src/Pure/Syntax/syntax.ML	Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/Syntax/syntax.ML	Wed Nov 25 09:13:46 2009 +0100
@@ -499,7 +499,7 @@
         (("Ambiguous input" ^ Position.str_of pos ^
           "\nproduces " ^ string_of_int len ^ " parse trees" ^
           (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
-          map show_pt ((uncurry take) (limit, pts)))));
+          map show_pt (take limit pts))));
     SynTrans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
   end;
 
@@ -545,7 +545,7 @@
         else cat_error (ambig_msg ()) (cat_lines
           (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
-            map (Pretty.string_of_term pp) ((uncurry take) (limit, results))))
+            map (Pretty.string_of_term pp) (take limit results)))
       end;
 
 fun standard_parse_term pp check get_sort map_const map_free map_type map_sort