# HG changeset patch
# User wenzelm
# Date 1309982572 -7200
# Node ID 5c9160f420d5c29a482de0d3bec6271f8cddb721
# Parent  85388f5570c4ed73a9122079e6094b297f327aa8
clarified record syntax: fieldext excludes the "more" pseudo-field (unlike 2f885b7e5ba7), so that errors like (| x = a, more = b |) are reported less confusingly;

diff -r 85388f5570c4 -r 5c9160f420d5 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Jul 06 20:46:06 2011 +0200
+++ b/src/HOL/Tools/record.ML	Wed Jul 06 22:02:52 2011 +0200
@@ -2411,7 +2411,7 @@
       |> add_extsplit extension_name ext_split
       |> add_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
       |> add_extfields extension_name (fields @ [(full_moreN, moreT)])
-      |> add_fieldext (extension_name, snd extension) (names @ [full_moreN])
+      |> add_fieldext (extension_name, snd extension) names
       |> add_code ext_tyco vs extT ext simps' ext_inject
       |> Sign.restore_naming thy;