Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/record_package.ML
changeset 17600 9ae09014730c
parent 17510 5e3ce025e1a5
child 17616 f526e2b9fe9e 
--- a/src/HOL/Tools/record_package.ML	Fri Sep 23 15:32:42 2005 +0200
+++ b/src/HOL/Tools/record_package.ML	Fri Sep 23 15:38:22 2005 +0200
@@ -644,7 +644,7 @@
   let
     fun field_lst t =
       (case strip_comb t of
-        (Const (ext,_),args)
+        (Const (ext,_),args as (_::_))
          => (case try (unsuffix extN) (Sign.intern_const sg ext) of
                SOME ext'
                => (case get_extfields sg ext' of
isabelle