# HG changeset patch
# User wenzelm
# Date 1236852602 -3600
# Node ID 5f31e24937c5895be2b769c5a5f693de8719b3e1
# Parent  038839f111a17944b64415c383934f9580fce85a
renamed NameSpace.bind to NameSpace.define;

diff -r 038839f111a1 -r 5f31e24937c5 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Mar 12 11:09:26 2009 +0100
+++ b/src/Pure/Isar/attrib.ML	Thu Mar 12 11:10:02 2009 +0100
@@ -146,7 +146,7 @@
   let
     val new_attrs =
       raw_attrs |> map (fn (name, att, comment) => (Binding.name name, ((att, comment), stamp ())));
-    fun add attrs = fold (snd oo NameSpace.bind (Sign.naming_of thy)) new_attrs attrs
+    fun add attrs = fold (snd oo NameSpace.define (Sign.naming_of thy)) new_attrs attrs
       handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup);
   in Attributes.map add thy end;
 
diff -r 038839f111a1 -r 5f31e24937c5 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Mar 12 11:09:26 2009 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Mar 12 11:10:02 2009 +0100
@@ -161,7 +161,7 @@
   | NONE => error ("Unknown locale " ^ quote name);
 
 fun register_locale binding parameters spec intros axioms decls notes dependencies thy =
-  thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (binding,
+  thy |> LocalesData.map (NameSpace.define (Sign.naming_of thy) (binding,
     mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies))) #> snd);
 
 fun change_locale name =
diff -r 038839f111a1 -r 5f31e24937c5 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Mar 12 11:09:26 2009 +0100
+++ b/src/Pure/Isar/method.ML	Thu Mar 12 11:10:02 2009 +0100
@@ -394,7 +394,7 @@
     val new_meths = raw_meths |> map (fn (name, f, comment) =>
       (Binding.name name, ((f, comment), stamp ())));
 
-    fun add meths = fold (snd oo NameSpace.bind (Sign.naming_of thy)) new_meths meths
+    fun add meths = fold (snd oo NameSpace.define (Sign.naming_of thy)) new_meths meths
       handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup);
   in Methods.map add thy end;
 
diff -r 038839f111a1 -r 5f31e24937c5 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Thu Mar 12 11:09:26 2009 +0100
+++ b/src/Pure/consts.ML	Thu Mar 12 11:10:02 2009 +0100
@@ -215,7 +215,7 @@
 fun err_dup_const c =
   error ("Duplicate declaration of constant " ^ quote c);
 
-fun extend_decls naming decl tab = NameSpace.bind naming decl tab
+fun extend_decls naming decl tab = NameSpace.define naming decl tab
   handle Symtab.DUP c => err_dup_const c;
 
 
diff -r 038839f111a1 -r 5f31e24937c5 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Mar 12 11:09:26 2009 +0100
+++ b/src/Pure/simplifier.ML	Thu Mar 12 11:10:02 2009 +0100
@@ -222,7 +222,7 @@
         val simproc' = morph_simproc phi simproc;
       in
         Simprocs.map (fn simprocs =>
-          NameSpace.bind naming (b', simproc') simprocs |> snd
+          NameSpace.define naming (b', simproc') simprocs |> snd
             handle Symtab.DUP dup => err_dup_simproc dup)
         #> map_ss (fn ss => ss addsimprocs [simproc'])
       end)
diff -r 038839f111a1 -r 5f31e24937c5 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Mar 12 11:09:26 2009 +0100
+++ b/src/Pure/theory.ML	Thu Mar 12 11:10:02 2009 +0100
@@ -175,7 +175,7 @@
 fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
   let
     val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
-    val axioms' = fold (snd oo NameSpace.bind (Sign.naming_of thy)) axms axioms
+    val axioms' = fold (snd oo NameSpace.define (Sign.naming_of thy)) axms axioms
       handle Symtab.DUP dup => err_dup_axm dup;
   in axioms' end);
 
diff -r 038839f111a1 -r 5f31e24937c5 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Mar 12 11:09:26 2009 +0100
+++ b/src/Pure/thm.ML	Thu Mar 12 11:10:02 2009 +0100
@@ -1700,7 +1700,7 @@
 fun add_oracle (b, oracle) thy =
   let
     val naming = Sign.naming_of thy;
-    val (name, tab') = NameSpace.bind naming (b, serial ()) (Oracles.get thy)
+    val (name, tab') = NameSpace.define naming (b, serial ()) (Oracles.get thy)
       handle Symtab.DUP _ => err_dup_ora (Binding.str_of b);
     val thy' = Oracles.put tab' thy;
   in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;