Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
bugfix in record_tr'
authorschirmer
Fri, 23 Sep 2005 15:38:22 +0200
changeset 17600 9ae09014730c
parent 17599 4da04f70221f
child 17601 a6a322f96145
bugfix in record_tr'
src/HOL/Tools/record_package.ML file | annotate | diff | comparison | revisions 
--- 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