# HG changeset patch
# User ballarin
# Date 1229681371 -3600
# Node ID 93ef3ae2b9e5cc55120f8fce9f3c22424885e56d
# Parent  e190bc2a53992f4e23431e9d4024e2d4b5a0a8f0# Parent  1ec081e2eae9992db187623412457b41ef610453
Merged.

diff -r e190bc2a5399 -r 93ef3ae2b9e5 src/Pure/Isar/new_locale.ML
--- 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;