Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned function name
authorhaftmann
Sat, 26 Jul 2008 09:00:26 +0200
changeset 27686 d1dbe31655be
parent 27685 cd561f58076d
child 27687 224a18d1a3ac
tuned function name
src/Pure/Isar/locale.ML file | annotate | diff | comparison | revisions 
--- 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))),
isabelle