src/Pure/variable.ML

--- a/src/Pure/variable.ML	Mon Oct 13 21:57:40 2014 +0200
+++ b/src/Pure/variable.ML	Mon Oct 13 22:43:29 2014 +0200
@@ -380,11 +380,11 @@
 fun new_fixed ((x, x'), pos) ctxt =
   if is_some (lookup_fixed ctxt x') then err_dups [Binding.make (x, pos)]
   else
-    let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.default_naming) in
+    let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming) in
       ctxt
       |> map_fixes
         (Name_Space.define context true (Binding.make (x', pos), x) #> snd #>
-          Name_Space.alias_table Name_Space.default_naming (Binding.make (x, pos)) x')
+          Name_Space.alias_table Name_Space.global_naming (Binding.make (x, pos)) x')
       |> declare_fixed x
       |> declare_constraints (Syntax.free x')
   end;