1.1 --- a/src/HOL/Tools/record.ML	Sat Mar 17 13:06:23 2012 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Mar 17 14:01:09 2012 +0100
     1.3 @@ -2225,13 +2225,12 @@
     1.4          Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt)
     1.5        | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T));
     1.6  
     1.7 -fun prep_field prep (x, T, mx) = (x, prep T, mx)
     1.8 -  handle ERROR msg =>
     1.9 -    cat_error msg ("The error(s) above occurred in record field " ^ Binding.print x);
    1.10 -
    1.11 -fun read_field raw_field ctxt =
    1.12 -  let val field as (_, T, _) = prep_field (Syntax.read_typ ctxt) raw_field
    1.13 -  in (field, Variable.declare_typ T ctxt) end;
    1.14 +fun read_fields raw_fields ctxt =
    1.15 +  let
    1.16 +    val Ts = Syntax.read_typs ctxt (map (fn (_, raw_T, _) => raw_T) raw_fields);
    1.17 +    val fields = map2 (fn (x, _, mx) => fn T => (x, T, mx)) raw_fields Ts;
    1.18 +    val ctxt' = fold Variable.declare_typ Ts ctxt;
    1.19 +  in (fields, ctxt') end;
    1.20  
    1.21  in
    1.22  
    1.23 @@ -2252,7 +2251,11 @@
    1.24      val parent_args = (case parent of SOME (Ts, _) => Ts | NONE => []);
    1.25      val parents = get_parent_info thy parent;
    1.26  
    1.27 -    val bfields = map (prep_field cert_typ) raw_fields;
    1.28 +    val bfields =
    1.29 +      raw_fields |> map (fn (x, raw_T, mx) => (x, cert_typ raw_T, mx)
    1.30 +        handle ERROR msg =>
    1.31 +          cat_error msg ("The error(s) above occurred in record field " ^ Binding.print x));
    1.32 +
    1.33  
    1.34      (* errors *)
    1.35  
    1.36 @@ -2293,7 +2296,7 @@
    1.37      val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
    1.38      val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
    1.39      val (parent, ctxt2) = read_parent raw_parent ctxt1;
    1.40 -    val (fields, ctxt3) = fold_map read_field raw_fields ctxt2;
    1.41 +    val (fields, ctxt3) = read_fields raw_fields ctxt2;
    1.42      val params' = map (Proof_Context.check_tfree ctxt3) params;
    1.43    in thy |> add_record (params', binding) parent fields end;
    1.44