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