Re: [isabelle] print_classes and records



On Fri, 19 Mar 2010, Mathieu Giorgino wrote:

I have a strange error when using the command "print_classes" after an extended record definition. Is this a bug ?

Yes, this problem was introduced in the last major overhaul of the record package, shortly before the release. It was fixed later, see http://isabelle.in.tum.de/repos/isabelle/rev/61bb9f8af129

The included diff is a backported version of that change. You can use the GNU patch utility to apply it to the Isabelle2009-1 sources.


	Makarius
diff -r 6a973bd43949 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Dec 02 12:04:07 2009 +0100
+++ b/src/HOL/Tools/record.ML	Sat Mar 20 16:45:22 2010 +0100
@@ -951,11 +951,11 @@
 
     fun field_lst 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 flds =>
+                SOME (flds as _ :: _) =>
                   (case get_fieldext thy (fst (hd flds)) of
                     SOME (_, alphas) =>
                      (let
@@ -968,9 +968,9 @@
                         val flds'' = (map o apsnd) (Envir.norm_type subst o varifyT) flds';
                       in flds'' @ field_lst more end
                       handle Type.TYPE_MATCH => [("", T)] | Library.UnequalLengths => [("", T)])
-                  | NONE => [("", T)])
-              | NONE => [("", T)])
-          | NONE => [("", T)])
+                  | _ => [("", T)])
+              | _ => [("", T)])
+          | _ => [("", T)])
       | _ => [("", T)]);
 
     val (flds, (_, moreT)) = split_last (field_lst T);


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.