src/HOL/Tools/record.ML
changeset 35615 61bb9f8af129
parent 35614 d7afa8700622
child 35625 9c818cab0dd0
--- a/src/HOL/Tools/record.ML	Sat Mar 06 16:13:22 2010 +0100
+++ b/src/HOL/Tools/record.ML	Sat Mar 06 17:32:45 2010 +0100
@@ -859,12 +859,12 @@
 
     fun strip_fields T =
       (case T of
-        Type (ext, args) =>
+        Type (ext, args as _ :: _) =>
           (case try (unsuffix ext_typeN) ext of
             SOME ext' =>
               (case get_extfields thy ext' of
-                SOME fields =>
-                  (case get_fieldext thy (fst (hd fields)) of
+                SOME (fields as (x, _) :: _) =>
+                  (case get_fieldext thy x of
                     SOME (_, alphas) =>
                      (let
                         val f :: fs = but_last fields;
@@ -877,9 +877,9 @@
                       in fields'' @ strip_fields more end
                       handle Type.TYPE_MATCH => [("", T)]
                         | Library.UnequalLengths => [("", T)])
-                  | NONE => [("", T)])
-              | NONE => [("", T)])
-          | NONE => [("", T)])
+                  | _ => [("", T)])
+              | _ => [("", T)])
+          | _ => [("", T)])
       | _ => [("", T)]);
 
     val (fields, (_, moreT)) = split_last (strip_fields T);