clarified record syntax: fieldext excludes the "more" pseudo-field (unlike 2f885b7e5ba7), so that errors like (| x = a, more = b |) are reported less confusingly;
1.1 --- a/src/HOL/Tools/record.ML Wed Jul 06 20:46:06 2011 +0200
1.2 +++ b/src/HOL/Tools/record.ML Wed Jul 06 22:02:52 2011 +0200
1.3 @@ -2411,7 +2411,7 @@
1.4 |> add_extsplit extension_name ext_split
1.5 |> add_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
1.6 |> add_extfields extension_name (fields @ [(full_moreN, moreT)])
1.7 - |> add_fieldext (extension_name, snd extension) (names @ [full_moreN])
1.8 + |> add_fieldext (extension_name, snd extension) names
1.9 |> add_code ext_tyco vs extT ext simps' ext_inject
1.10 |> Sign.restore_naming thy;
1.11