--- 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;