# HG changeset patch
# User wenzelm
# Date 1309179668 -7200
# Node ID 94a08fb3ae4a7774d6fe3ffda688b1f922298485
# Parent  844b4a178dffb2d34f388b69f8933e998ee0a1ad
parallel Syntax.parse, which is rather slow;

diff -r 844b4a178dff -r 94a08fb3ae4a src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Jun 27 14:38:58 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Jun 27 15:01:08 2011 +0200
@@ -369,8 +369,8 @@
 fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt;
 fun read_typ ctxt = parse_typ ctxt #> singleton (check_typs ctxt);
 
-fun read_terms ctxt = map (parse_term ctxt) #> check_terms ctxt;
-fun read_props ctxt = map (parse_prop ctxt) #> check_props ctxt;
+fun read_terms ctxt = Par_List.map_name "Syntax.read_terms" (parse_term ctxt) #> check_terms ctxt;
+fun read_props ctxt = Par_List.map_name "Syntax.read_props" (parse_prop ctxt) #> check_props ctxt;
 
 val read_term = singleton o read_terms;
 val read_prop = singleton o read_props;