# HG changeset patch
# User wenzelm
# Date 1267893165 -3600
# Node ID 61bb9f8af129c57b30298552110c778c7d20a7fe
# Parent  d7afa87006220696e8b6f737f270423679888298
record_type_tr': more robust strip_fields (printed types are not necessarily well-formed, e.g. in Syntax.pretty_arity);

diff -r d7afa8700622 -r 61bb9f8af129 src/HOL/Tools/record.ML
--- 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);