1.1 --- a/src/Pure/Isar/locale.ML	Sat Jul 26 09:00:25 2008 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Sat Jul 26 09:00:26 2008 +0200
     1.3 @@ -391,7 +391,7 @@
     1.4   of SOME loc => loc
     1.5    | NONE => error ("Unknown locale " ^ quote name);
     1.6  
     1.7 -fun add_locale name loc thy =
     1.8 +fun register_locale name loc thy =
     1.9    thy |> LocalesData.map (fn (space, locs) =>
    1.10      (Sign.declare_name thy name space, Symtab.update (name, loc) locs));
    1.11  
    1.12 @@ -1949,7 +1949,7 @@
    1.13      val axs' = map (Element.assume_witness thy') stmt';
    1.14      val loc_ctxt = thy'
    1.15        |> PureThy.note_thmss_qualified Thm.assumptionK bname facts' |> snd
    1.16 -      |> add_locale name {axiom = axs',
    1.17 +      |> register_locale name {axiom = axs',
    1.18          imports = empty,
    1.19          elems = map (fn e => (e, stamp ())) elems'',
    1.20          params = params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),