1.1 --- a/src/Pure/Isar/specification.ML	Sat Mar 17 12:52:40 2012 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Sat Mar 17 13:06:23 2012 +0100
     1.3 @@ -119,7 +119,8 @@
     1.4  
     1.5      val Asss =
     1.6        (map o map) snd raw_specss
     1.7 -      |> (burrow o burrow) (Par_List.map_name "Specification.parse_prop" (parse_prop params_ctxt));
     1.8 +      |> (burrow o burrow)
     1.9 +        (grouped 10 (Par_List.map_name "Specification.parse_prop") (parse_prop params_ctxt));
    1.10      val names = Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss)
    1.11        |> fold Name.declare xs;
    1.12      val Asss' = #1 ((fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss names);

     2.1 --- a/src/Pure/Syntax/syntax.ML	Sat Mar 17 12:52:40 2012 +0100
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Mar 17 13:06:23 2012 +0100
     2.3 @@ -43,6 +43,7 @@
     2.4    val read_typ: Proof.context -> string -> typ
     2.5    val read_term: Proof.context -> string -> term
     2.6    val read_prop: Proof.context -> string -> term
     2.7 +  val read_typs: Proof.context -> string list -> typ list
     2.8    val read_terms: Proof.context -> string list -> term list
     2.9    val read_props: Proof.context -> string list -> term list
    2.10    val read_sort_global: theory -> string -> sort
    2.11 @@ -265,11 +266,17 @@
    2.12  (* read = parse + check *)
    2.13  
    2.14  fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt;
    2.15 -fun read_typ ctxt = parse_typ ctxt #> singleton (check_typs ctxt);
    2.16  
    2.17 -fun read_terms ctxt = Par_List.map_name "Syntax.read_terms" (parse_term ctxt) #> check_terms ctxt;
    2.18 -fun read_props ctxt = Par_List.map_name "Syntax.read_props" (parse_prop ctxt) #> check_props ctxt;
    2.19 +fun read_typs ctxt =
    2.20 +  grouped 10 (Par_List.map_name "Syntax.read_typs") (parse_typ ctxt) #> check_typs ctxt;
    2.21  
    2.22 +fun read_terms ctxt =
    2.23 +  grouped 10 (Par_List.map_name "Syntax.read_terms") (parse_term ctxt) #> check_terms ctxt;
    2.24 +
    2.25 +fun read_props ctxt =
    2.26 +  grouped 10 (Par_List.map_name "Syntax.read_props") (parse_prop ctxt) #> check_props ctxt;
    2.27 +
    2.28 +val read_typ = singleton o read_typs;
    2.29  val read_term = singleton o read_terms;
    2.30  val read_prop = singleton o read_props;
    2.31  

     3.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sat Mar 17 12:52:40 2012 +0100
     3.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sat Mar 17 13:06:23 2012 +0100
     3.3 @@ -360,7 +360,7 @@
     3.4  
     3.5            val results' =
     3.6              if parsed_len > 1 then
     3.7 -              (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result)
     3.8 +              (grouped 10 (Par_List.map_name "Syntax_Phases.parse_term") o apsnd o Exn.maps_result)
     3.9                  check results
    3.10              else results;
    3.11            val reports' = fst (hd results');