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