1.1 --- a/src/Pure/Syntax/syntax.ML Sat Mar 17 12:52:40 2012 +0100
1.2 +++ b/src/Pure/Syntax/syntax.ML Sat Mar 17 13:06:23 2012 +0100
1.3 @@ -43,6 +43,7 @@
1.4 val read_typ: Proof.context -> string -> typ
1.5 val read_term: Proof.context -> string -> term
1.6 val read_prop: Proof.context -> string -> term
1.7 + val read_typs: Proof.context -> string list -> typ list
1.8 val read_terms: Proof.context -> string list -> term list
1.9 val read_props: Proof.context -> string list -> term list
1.10 val read_sort_global: theory -> string -> sort
1.11 @@ -265,11 +266,17 @@
1.12 (* read = parse + check *)
1.13
1.14 fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt;
1.15 -fun read_typ ctxt = parse_typ ctxt #> singleton (check_typs ctxt);
1.16
1.17 -fun read_terms ctxt = Par_List.map_name "Syntax.read_terms" (parse_term ctxt) #> check_terms ctxt;
1.18 -fun read_props ctxt = Par_List.map_name "Syntax.read_props" (parse_prop ctxt) #> check_props ctxt;
1.19 +fun read_typs ctxt =
1.20 + grouped 10 (Par_List.map_name "Syntax.read_typs") (parse_typ ctxt) #> check_typs ctxt;
1.21
1.22 +fun read_terms ctxt =
1.23 + grouped 10 (Par_List.map_name "Syntax.read_terms") (parse_term ctxt) #> check_terms ctxt;
1.24 +
1.25 +fun read_props ctxt =
1.26 + grouped 10 (Par_List.map_name "Syntax.read_props") (parse_prop ctxt) #> check_props ctxt;
1.27 +
1.28 +val read_typ = singleton o read_typs;
1.29 val read_term = singleton o read_terms;
1.30 val read_prop = singleton o read_props;
1.31