Merged.

--- a/src/Pure/Isar/new_locale.ML	Fri Dec 19 11:09:09 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Fri Dec 19 11:09:31 2008 +0100
@@ -399,9 +399,15 @@
 
 val get_global_registrations =
   Context.Theory #> RegistrationsData.get #> map fst #> map (apsnd op $>);
-fun add_global_registration reg =
+
+fun add_global reg =
   (Context.theory_map o RegistrationsData.map) (cons (reg, stamp ()));
 
+fun add_global_registration (name, (base_morph, export)) thy =
+  roundup thy (fn _ => fn (name', morph') => fn thy => add_global (name', (morph', export)) thy)
+    (name, base_morph) (get_global_idents thy, thy) |>
+    snd (* FIXME ?? uncurry put_global_idents *);
+
 fun amend_global_registration morph (name, base_morph) thy =
   let
     val regs = (Context.Theory #> RegistrationsData.get #> map fst) thy;