src/HOL/Tools/record.ML
changeset 35615 61bb9f8af129
parent 35614 d7afa8700622
child 35625 9c818cab0dd0
equal deleted inserted replaced
35614:d7afa8700622 35615:61bb9f8af129
   857 
   857 
   858     val term_of_type = Syntax.term_of_typ (! Syntax.show_sorts);
   858     val term_of_type = Syntax.term_of_typ (! Syntax.show_sorts);
   859 
   859 
   860     fun strip_fields T =
   860     fun strip_fields T =
   861       (case T of
   861       (case T of
   862         Type (ext, args) =>
   862         Type (ext, args as _ :: _) =>
   863           (case try (unsuffix ext_typeN) ext of
   863           (case try (unsuffix ext_typeN) ext of
   864             SOME ext' =>
   864             SOME ext' =>
   865               (case get_extfields thy ext' of
   865               (case get_extfields thy ext' of
   866                 SOME fields =>
   866                 SOME (fields as (x, _) :: _) =>
   867                   (case get_fieldext thy (fst (hd fields)) of
   867                   (case get_fieldext thy x of
   868                     SOME (_, alphas) =>
   868                     SOME (_, alphas) =>
   869                      (let
   869                      (let
   870                         val f :: fs = but_last fields;
   870                         val f :: fs = but_last fields;
   871                         val fields' =
   871                         val fields' =
   872                           apfst (Sign.extern_const thy) f :: map (apfst Long_Name.base_name) fs;
   872                           apfst (Sign.extern_const thy) f :: map (apfst Long_Name.base_name) fs;
   875                         val subst = fold (Sign.typ_match thy) (alphavars ~~ args') Vartab.empty;
   875                         val subst = fold (Sign.typ_match thy) (alphavars ~~ args') Vartab.empty;
   876                         val fields'' = (map o apsnd) (Envir.norm_type subst o varifyT) fields';
   876                         val fields'' = (map o apsnd) (Envir.norm_type subst o varifyT) fields';
   877                       in fields'' @ strip_fields more end
   877                       in fields'' @ strip_fields more end
   878                       handle Type.TYPE_MATCH => [("", T)]
   878                       handle Type.TYPE_MATCH => [("", T)]
   879                         | Library.UnequalLengths => [("", T)])
   879                         | Library.UnequalLengths => [("", T)])
   880                   | NONE => [("", T)])
   880                   | _ => [("", T)])
   881               | NONE => [("", T)])
   881               | _ => [("", T)])
   882           | NONE => [("", T)])
   882           | _ => [("", T)])
   883       | _ => [("", T)]);
   883       | _ => [("", T)]);
   884 
   884 
   885     val (fields, (_, moreT)) = split_last (strip_fields T);
   885     val (fields, (_, moreT)) = split_last (strip_fields T);
   886     val _ = null fields andalso raise Match;
   886     val _ = null fields andalso raise Match;
   887     val u = foldr1 field_types_tr' (map (field_type_tr' o apsnd term_of_type) fields);
   887     val u = foldr1 field_types_tr' (map (field_type_tr' o apsnd term_of_type) fields);