# HG changeset patch
# User ballarin
# Date 1229681256 -3600
# Node ID 1ec081e2eae9992db187623412457b41ef610453
# Parent  918687637307cdedf9b9c5ae9fc4f416b2c95cc6
Add inherited registrations.

diff -r 918687637307 -r 1ec081e2eae9 src/Pure/Isar/new_locale.ML
--- a/src/Pure/Isar/new_locale.ML	Thu Dec 18 19:52:11 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Fri Dec 19 11:07:36 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;