src/Pure/variable.ML

 sig
   val is_body: Proof.context -> bool
   val set_body: bool -> Proof.context -> Proof.context
   val restore_body: Proof.context -> Proof.context -> Proof.context
   val names_of: Proof.context -> Name.context
-  val fixes_of: Proof.context -> (string * string) list
   val binds_of: Proof.context -> (typ * term) Vartab.table
   val maxidx_of: Proof.context -> int
   val sorts_of: Proof.context -> sort list
   val constraints_of: Proof.context -> typ Vartab.table * sort Vartab.table
   val is_declared: Proof.context -> string -> bool
-  val is_fixed: Proof.context -> string -> bool
-  val newly_fixed: Proof.context -> Proof.context -> string -> bool
   val name: binding -> string
   val default_type: Proof.context -> string -> typ option
   val def_type: Proof.context -> bool -> indexname -> typ option
   val def_sort: Proof.context -> indexname -> sort option
   val declare_names: term -> Proof.context -> Proof.context

   val bind_term: indexname * term option -> Proof.context -> Proof.context
   val expand_binds: Proof.context -> term -> term
   val lookup_const: Proof.context -> string -> string option
   val is_const: Proof.context -> string -> bool
   val declare_const: string * string -> Proof.context -> Proof.context
+  val fixed_ord: Proof.context -> string * string -> order
+  val is_fixed: Proof.context -> string -> bool
+  val newly_fixed: Proof.context -> Proof.context -> string -> bool
+  val intern_fixed: Proof.context -> string -> string
+  val lookup_fixed: Proof.context -> string -> string option
+  val revert_fixed: Proof.context -> string -> string
   val add_fixed_names: Proof.context -> term -> string list -> string list
   val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list
   val add_free_names: Proof.context -> term -> string list -> string list
   val add_frees: Proof.context -> term -> (string * typ) list -> (string * typ) list
+  val add_fixes_binding: binding list -> Proof.context -> string list * Proof.context
   val add_fixes: string list -> Proof.context -> string list * Proof.context
   val add_fixes_direct: string list -> Proof.context -> Proof.context
   val auto_fixes: term -> Proof.context -> Proof.context
   val variant_fixes: string list -> Proof.context -> string list * Proof.context
+  val dest_fixes: Proof.context -> (string * string) list
   val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
   val export_terms: Proof.context -> Proof.context -> term list -> term list
   val exportT_terms: Proof.context -> Proof.context -> term list -> term list
   val exportT: Proof.context -> Proof.context -> thm list -> thm list
   val export_prf: Proof.context -> Proof.context -> Proofterm.proof -> Proofterm.proof

 structure Variable: VARIABLE =
 struct
 
 (** local context data **)
 
+type fixes = string Name_Space.table;
+val empty_fixes: fixes = Name_Space.empty_table "fixed variable";
+
 datatype data = Data of
  {is_body: bool,                        (*inner body mode*)
   names: Name.context,                  (*type/term variable names*)
   consts: string Symtab.table,          (*consts within the local scope*)
-  fixes: (string * string) list,        (*term fixes -- extern/intern*)
+  fixes: fixes,                         (*term fixes -- global name space, intern ~> extern*)
   binds: (typ * term) Vartab.table,     (*term bindings*)
   type_occs: string list Symtab.table,  (*type variables -- possibly within term variables*)
   maxidx: int,                          (*maximum var index*)
   sorts: sort Ord_List.T,               (*declared sort occurrences*)
   constraints:

 
 structure Data = Proof_Data
 (
   type T = data;
   fun init _ =
-    make_data (false, Name.context, Symtab.empty, [], Vartab.empty, Symtab.empty,
-      ~1, [], (Vartab.empty, Vartab.empty));
+    make_data (false, Name.context, Symtab.empty, empty_fixes, Vartab.empty,
+      Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty));
 );
 
 fun map_data f =
   Data.map (fn Data {is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints} =>
     make_data (f (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints)));

 val maxidx_of = #maxidx o rep_data;
 val sorts_of = #sorts o rep_data;
 val constraints_of = #constraints o rep_data;
 
 val is_declared = Name.is_declared o names_of;
-fun is_fixed ctxt x = exists (fn (_, y) => x = y) (fixes_of ctxt);
-fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);
 
 (*checked name binding*)
 val name = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming;
 
 

 
 
 
 (** fixes **)
 
+(* specialized name space *)
+
+fun fixed_ord ctxt = Name_Space.entry_ord (#1 (fixes_of ctxt));
+
+fun is_fixed ctxt x = can (Name_Space.the_entry (#1 (fixes_of ctxt))) x;
+fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);
+
+fun intern_fixed ctxt = Name_Space.intern (#1 (fixes_of ctxt));
+
+fun lookup_fixed ctxt x =
+  let val x' = intern_fixed ctxt x
+  in if is_fixed ctxt x' then SOME x' else NONE end;
+
+fun revert_fixed ctxt x =
+  (case Symtab.lookup (#2 (fixes_of ctxt)) x of
+    SOME x' => if intern_fixed ctxt x' = x then x' else x
+  | NONE => x);
+
+fun dest_fixes ctxt =
+  let val (space, tab) = fixes_of ctxt
+  in sort (Name_Space.entry_ord space o pairself #2) (map swap (Symtab.dest tab)) end;
+
+
 (* collect variables *)
 
 fun add_free_names ctxt =
   fold_aterms (fn Free (x, _) => not (is_fixed ctxt x) ? insert (op =) x | _ => I);
 

 
 (* declarations *)
 
 local
 
-fun no_dups [] = ()
-  | no_dups dups = error ("Duplicate fixed variable(s): " ^ commas_quote dups);
-
-fun new_fixes names' xs xs' =
+fun err_dups dups =
+  error ("Duplicate fixed variable(s): " ^ commas (map Binding.print dups));
+
+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');
+
+fun new_fixes names' xs xs' ps =
   map_names (K names') #>
-  fold declare_fixed xs #>
-  map_fixes (fn fixes => (rev (xs ~~ xs') @ fixes)) #>
-  fold (declare_constraints o Syntax.free) xs' #>
+  fold new_fixed ((xs ~~ xs') ~~ ps) #>
   pair xs';
 
 in
 
-fun add_fixes xs ctxt =
+fun add_fixes_binding bs ctxt =
   let
     val _ =
-      (case filter (can Name.dest_skolem) xs of [] => ()
-      | bads => error ("Illegal internal Skolem constant(s): " ^ commas_quote bads));
-    val _ = no_dups (duplicates (op =) xs);
-    val (ys, zs) = split_list (fixes_of ctxt);
+      (case filter (can Name.dest_skolem o Binding.name_of) bs of
+        [] => ()
+      | bads => error ("Illegal internal Skolem constant(s): " ^ commas (map Binding.print bads)));
+    val _ =
+      (case duplicates (op = o pairself Binding.name_of) bs of
+        [] => ()
+      | dups => err_dups dups);
+
+    val xs = map name bs;
     val names = names_of ctxt;
     val (xs', names') =
       if is_body ctxt then Name.variants xs names |>> map Name.skolem
-      else (no_dups (inter (op =) xs ys); no_dups (inter (op =) xs zs);
-        (xs, fold Name.declare xs names));
-  in ctxt |> new_fixes names' xs xs' end;
+      else (xs, fold Name.declare xs names);
+  in ctxt |> new_fixes names' xs xs' (map Binding.pos_of bs) end;
 
 fun variant_fixes raw_xs ctxt =
   let
     val names = names_of ctxt;
     val xs = map (fn x => Name.clean x |> can Name.dest_internal x ? Name.internal) raw_xs;
     val (xs', names') = Name.variants xs names |>> (is_body ctxt ? map Name.skolem);
-  in ctxt |> new_fixes names' xs xs' end;
+  in ctxt |> new_fixes names' xs xs' (replicate (length xs) Position.none) end;
 
 end;
 
+val add_fixes = add_fixes_binding o map Binding.name;
 
 fun add_fixes_direct xs ctxt = ctxt
   |> set_body false
   |> (snd o add_fixes xs)
   |> restore_body ctxt;

 (** export -- generalize type/term variables (beware of closure sizes) **)
 
 fun export_inst inner outer =
   let
     val declared_outer = is_declared outer;
-    val fixes_inner = fixes_of inner;
-    val fixes_outer = fixes_of outer;
-
-    val gen_fixes = map #2 (take (length fixes_inner - length fixes_outer) fixes_inner);
+
+    val gen_fixes =
+      Symtab.fold (fn (y, _) => not (is_fixed outer y) ? cons y)
+        (#2 (fixes_of inner)) [];
     val still_fixed = not o member (op =) gen_fixes;
 
     val type_occs_inner = type_occs_of inner;
     fun gen_fixesT ts =
       Symtab.fold (fn (a, xs) =>