1.1 --- a/src/HOL/Tools/record.ML	Wed Jul 06 09:54:40 2011 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Wed Jul 06 11:37:29 2011 +0200
     1.3 @@ -670,6 +670,15 @@
     1.4  
     1.5  local
     1.6  
     1.7 +fun split_args (field :: fields) ((name, arg) :: fargs) =
     1.8 +      if can (unsuffix name) field then
     1.9 +        let val (args, rest) = split_args fields fargs
    1.10 +        in (arg :: args, rest) end
    1.11 +      else raise Fail ("expecting field " ^ quote field ^ " but got " ^ quote name)
    1.12 +  | split_args [] (fargs as (_ :: _)) = ([], fargs)
    1.13 +  | split_args (_ :: _) [] = raise Fail "expecting more fields"
    1.14 +  | split_args _ _ = ([], []);
    1.15 +
    1.16  fun field_type_tr ((Const (@{syntax_const "_field_type"}, _) $ Const (name, _) $ arg)) =
    1.17        (name, arg)
    1.18    | field_type_tr t = raise TERM ("field_type_tr", [t]);
    1.19 @@ -683,15 +692,6 @@
    1.20      val thy = Proof_Context.theory_of ctxt;
    1.21      fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]);
    1.22  
    1.23 -    fun split_args (field :: fields) ((name, arg) :: fargs) =
    1.24 -          if can (unsuffix name) field then
    1.25 -            let val (args, rest) = split_args fields fargs
    1.26 -            in (arg :: args, rest) end
    1.27 -          else err ("expecting field " ^ field ^ " but got " ^ name)
    1.28 -      | split_args [] (fargs as (_ :: _)) = ([], fargs)
    1.29 -      | split_args (_ :: _) [] = err "expecting more fields"
    1.30 -      | split_args _ _ = ([], []);
    1.31 -
    1.32      fun mk_ext (fargs as (name, _) :: _) =
    1.33            (case get_fieldext thy (Proof_Context.intern_const ctxt name) of
    1.34              SOME (ext, alphas) =>
    1.35 @@ -700,7 +700,8 @@
    1.36                    let
    1.37                      val (fields', _) = split_last fields;
    1.38                      val types = map snd fields';
    1.39 -                    val (args, rest) = split_args (map fst fields') fargs;
    1.40 +                    val (args, rest) = split_args (map fst fields') fargs
    1.41 +                      handle Fail msg => err msg;
    1.42                      val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
    1.43                      val midx = fold Term.maxidx_typ argtypes 0;
    1.44                      val varifyT = varifyT midx;
    1.45 @@ -742,23 +743,14 @@
    1.46      val thy = Proof_Context.theory_of ctxt;
    1.47      fun err msg = raise TERM ("Error in record input: " ^ msg, [t]);
    1.48  
    1.49 -    fun split_args (field :: fields) ((name, arg) :: fargs) =
    1.50 -          if can (unsuffix name) field
    1.51 -          then
    1.52 -            let val (args, rest) = split_args fields fargs
    1.53 -            in (arg :: args, rest) end
    1.54 -          else err ("expecting field " ^ field ^ " but got " ^ name)
    1.55 -      | split_args [] (fargs as (_ :: _)) = ([], fargs)
    1.56 -      | split_args (_ :: _) [] = err "expecting more fields"
    1.57 -      | split_args _ _ = ([], []);
    1.58 -
    1.59      fun mk_ext (fargs as (name, _) :: _) =
    1.60            (case get_fieldext thy (Proof_Context.intern_const ctxt name) of
    1.61              SOME (ext, _) =>
    1.62                (case get_extfields thy ext of
    1.63                  SOME fields =>
    1.64                    let
    1.65 -                    val (args, rest) = split_args (map fst (fst (split_last fields))) fargs;
    1.66 +                    val (args, rest) = split_args (map fst (fst (split_last fields))) fargs
    1.67 +                      handle Fail msg => err msg;
    1.68                      val more' = mk_ext rest;
    1.69                    in list_comb (Syntax.const (Lexicon.mark_const (ext ^ extN)), args @ [more']) end
    1.70                | NONE => err ("no fields defined for " ^ ext))