--- a/src/Pure/variable.ML Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/variable.ML Sun Mar 18 13:04:22 2012 +0100
@@ -341,12 +341,14 @@
fun new_fixed ((x, x'), pos) ctxt =
if is_some (lookup_fixed ctxt x') then err_dups [Binding.make (x, pos)]
else
- ctxt
- |> map_fixes
- (Name_Space.define ctxt true Name_Space.default_naming (Binding.make (x', pos), x) #> snd #>>
- Name_Space.alias Name_Space.default_naming (Binding.make (x, pos)) x')
- |> declare_fixed x
- |> declare_constraints (Syntax.free x');
+ let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.default_naming) in
+ ctxt
+ |> map_fixes
+ (Name_Space.define context true (Binding.make (x', pos), x) #> snd #>>
+ Name_Space.alias Name_Space.default_naming (Binding.make (x, pos)) x')
+ |> declare_fixed x
+ |> declare_constraints (Syntax.free x')
+ end;
fun new_fixes names' xs xs' ps =
map_names (K names') #>