--- a/src/Pure/Tools/plugin.ML Mon Oct 13 21:57:40 2014 +0200
+++ b/src/Pure/Tools/plugin.ML Mon Oct 13 22:43:29 2014 +0200
@@ -54,7 +54,7 @@
fun define binding rhs thy =
let
- val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.default_naming);
+ val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming);
val (name, data') = Name_Space.define context true (binding, resolve thy rhs) (Data.get thy);
val thy' = Data.put data' thy;
in (name, thy') end;