# HG changeset patch
# User schirmer
# Date 1127482702 -7200
# Node ID 9ae09014730cb6066f809afa91bae85fc52acd15
# Parent  4da04f70221f2265f34b86594a3517d6f493a774
bugfix in record_tr'

diff -r 4da04f70221f -r 9ae09014730c src/HOL/Tools/record_package.ML
--- 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