src/HOL/Tools/record.ML
changeset 35615 61bb9f8af129
parent 35614 d7afa8700622
child 35625 9c818cab0dd0
     1.1 --- a/src/HOL/Tools/record.ML	Sat Mar 06 16:13:22 2010 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Mar 06 17:32:45 2010 +0100
     1.3 @@ -859,12 +859,12 @@
     1.4  
     1.5      fun strip_fields T =
     1.6        (case T of
     1.7 -        Type (ext, args) =>
     1.8 +        Type (ext, args as _ :: _) =>
     1.9            (case try (unsuffix ext_typeN) ext of
    1.10              SOME ext' =>
    1.11                (case get_extfields thy ext' of
    1.12 -                SOME fields =>
    1.13 -                  (case get_fieldext thy (fst (hd fields)) of
    1.14 +                SOME (fields as (x, _) :: _) =>
    1.15 +                  (case get_fieldext thy x of
    1.16                      SOME (_, alphas) =>
    1.17                       (let
    1.18                          val f :: fs = but_last fields;
    1.19 @@ -877,9 +877,9 @@
    1.20                        in fields'' @ strip_fields more end
    1.21                        handle Type.TYPE_MATCH => [("", T)]
    1.22                          | Library.UnequalLengths => [("", T)])
    1.23 -                  | NONE => [("", T)])
    1.24 -              | NONE => [("", T)])
    1.25 -          | NONE => [("", T)])
    1.26 +                  | _ => [("", T)])
    1.27 +              | _ => [("", T)])
    1.28 +          | _ => [("", T)])
    1.29        | _ => [("", T)]);
    1.30  
    1.31      val (fields, (_, moreT)) = split_last (strip_fields T);