# HG changeset patch
# User haftmann
# Date 1217055626 -7200
# Node ID d1dbe31655be88ea739f732f7bfe600acc4ac015
# Parent  cd561f58076d26336b0ea1d787af1be35103dc8e
tuned function name

diff -r cd561f58076d -r d1dbe31655be src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Jul 26 09:00:25 2008 +0200
+++ b/src/Pure/Isar/locale.ML	Sat Jul 26 09:00:26 2008 +0200
@@ -391,7 +391,7 @@
  of SOME loc => loc
   | NONE => error ("Unknown locale " ^ quote name);
 
-fun add_locale name loc thy =
+fun register_locale name loc thy =
   thy |> LocalesData.map (fn (space, locs) =>
     (Sign.declare_name thy name space, Symtab.update (name, loc) locs));
 
@@ -1949,7 +1949,7 @@
     val axs' = map (Element.assume_witness thy') stmt';
     val loc_ctxt = thy'
       |> PureThy.note_thmss_qualified Thm.assumptionK bname facts' |> snd
-      |> add_locale name {axiom = axs',
+      |> register_locale name {axiom = axs',
         imports = empty,
         elems = map (fn e => (e, stamp ())) elems'',
         params = params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),