# HG changeset patch
# User wenzelm
# Date 1303938268 -7200
# Node ID 9e1a77ad7ca37af5a071acc0950241376194a31d
# Parent  89acb654d8eb2298d8193af9d3ce766f76dff8eb# Parent  65ec88b369fdf7b7f45e56b84c2a1f8cda5879f9
merged

diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -92,7 +92,7 @@
     val finish_rule =
       split_all_tuples
       #> rename_params_rule true
-        (map (Name.clean o Proof_Context.revert_skolem defs_ctxt o fst) avoiding);
+        (map (Name.clean o Variable.revert_fixed defs_ctxt o fst) avoiding);
 
     fun rule_cases ctxt r =
       let val r' = if simp then Induct.simplified_rule ctxt r else r
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/HOL/Statespace/state_space.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -187,16 +187,11 @@
       Symtab.lookup (StateSpaceData.get ctxt) name;
 
 
-fun lookupI eq xs n =
-  (case AList.lookup eq xs n of
-     SOME v => v
-   | NONE => n);
-
 fun mk_free ctxt name =
   if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name
   then
-    let val n' = lookupI (op =) (Variable.fixes_of ctxt) name
-    in SOME (Free (n',Proof_Context.infer_type ctxt (n', dummyT))) end
+    let val n' = Variable.intern_fixed ctxt name
+    in SOME (Free (n', Proof_Context.infer_type ctxt (n', dummyT))) end
   else NONE
 
 
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Tools/Function/context_tree.ML
--- a/src/HOL/Tools/Function/context_tree.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/HOL/Tools/Function/context_tree.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -103,10 +103,10 @@
 (* Called on the INSTANTIATED branches of the congruence rule *)
 fun mk_branch ctxt t =
   let
-    val ((fixes, impl), ctxt') = Function_Lib.focus_term t ctxt
+    val ((params, impl), ctxt') = Variable.focus t ctxt
     val (assms, concl) = Logic.strip_horn impl
   in
-    (ctxt', fixes, assms, rhs_of concl)
+    (ctxt', map #2 params, assms, rhs_of concl)
   end
 
 fun find_cong_rule ctxt fvar h ((r,dep)::rs) t =
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -9,7 +9,6 @@
 sig
   val plural: string -> string -> 'a list -> string
 
-  val focus_term: term -> Proof.context -> ((string * typ) list * term) * Proof.context
   val dest_all_all: term -> term list * term
 
   val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
@@ -38,19 +37,6 @@
   | plural sg pl _ = pl
 
 
-(*term variant of Variable.focus*)
-fun focus_term t ctxt =
-  let
-    val ps = Term.variant_frees t (Term.strip_all_vars t);   (*as they are printed :-*)
-    val (xs, Ts) = split_list ps;
-    val (xs', ctxt') = Variable.variant_fixes xs ctxt;
-    val ps' = xs' ~~ Ts;
-    val inst = map Free ps'
-    val t' = Term.subst_bounds (rev inst, Term.strip_all_body t);
-    val ctxt'' = ctxt' |> fold Variable.declare_constraints inst;
-  in ((ps', t'), ctxt'') end;
-
-
 (* Removes all quantifiers from a term, replacing bound variables by frees. *)
 fun dest_all_all (t as (Const ("all",_) $ _)) =
   let
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -55,9 +55,9 @@
 
 fun dest_hhf ctxt t =
   let
-    val ((vars, imp), ctxt') = Function_Lib.focus_term t ctxt
+    val ((params, imp), ctxt') = Variable.focus t ctxt
   in
-    (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
+    (ctxt', map #2 params, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
   end
 
 fun mk_scheme' ctxt cases concl =
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -165,7 +165,7 @@
         "Known modes are " ^ commas_quote (known_modes lthy) ^ "."]);
 
     val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [eqn_raw] lthy;
-    val ((_, plain_eqn), _) = Function_Lib.focus_term eqn lthy;
+    val ((_, plain_eqn), _) = Variable.focus eqn lthy;
 
     val ((f_binding, fT), mixfix) = the_single fixes;
     val fname = Binding.name_of f_binding;
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -1047,15 +1047,14 @@
       end
   end
 
-fun is_fixed_equation fixes
+fun is_fixed_equation ctxt
                       (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) =
-    member (op =) fixes s
+    Variable.is_fixed ctxt s
   | is_fixed_equation _ _ = false
 fun extract_fixed_frees ctxt (assms, t) =
   let
-    val fixes = Variable.fixes_of ctxt |> map snd
     val (subst, other_assms) =
-      List.partition (is_fixed_equation fixes) assms
+      List.partition (is_fixed_equation ctxt) assms
       |>> map Logic.dest_equals
   in (subst, other_assms, subst_atomic subst t) end
 
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -956,7 +956,7 @@
     fun mk_insert x S =
       Const (@{const_name "Set.insert"}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S 
     fun mk_set_compr in_insert [] xs =
-       rev ((Free ("...", fastype_of t_compr)) ::
+       rev ((Free ("dots", fastype_of t_compr)) ::  (* FIXME proper name!? *)
         (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs))
       | mk_set_compr in_insert (t :: ts) xs =
         let
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -1902,7 +1902,7 @@
     val ((T, ts), statistics) = eval ctxt stats param_user_modes comp_options k t_compr
     val setT = HOLogic.mk_setT T
     val elems = HOLogic.mk_set T ts
-    val cont = Free ("...", setT)
+    val cont = Free ("dots", setT)  (* FIXME proper name!? *)
     (* check expected values *)
     val () =
       case raw_expected of
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -51,7 +51,7 @@
 
     fun sanity_test NONE _ = true
       | sanity_test (SOME bind) str =
-          if Variable.name bind = str then true
+          if Variable.check_name bind = str then true
           else error_msg bind str
 
     val _ = sanity_test optbind lhs_str
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/HOL/Tools/inductive.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -552,10 +552,10 @@
 val ind_cases_setup =
   Method.setup @{binding ind_cases}
     (Scan.lift (Scan.repeat1 Args.name_source --
-      Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) []) >>
+      Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.binding) []) >>
       (fn (raw_props, fixes) => fn ctxt =>
         let
-          val (_, ctxt') = Variable.add_fixes fixes ctxt;
+          val (_, ctxt') = Variable.add_fixes_binding fixes ctxt;
           val props = Syntax.read_props ctxt' raw_props;
           val ctxt'' = fold Variable.declare_term props ctxt';
           val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props)
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Pure/General/markup.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -36,7 +36,6 @@
   val hiddenN: string val hidden: T
   val tclassN: string val tclass: string -> T
   val tyconN: string val tycon: string -> T
-  val fixed_declN: string val fixed_decl: string -> T
   val fixedN: string val fixed: string -> T
   val constN: string val const: string -> T
   val dynamic_factN: string val dynamic_fact: string -> T
@@ -209,7 +208,6 @@
 
 val (tclassN, tclass) = markup_string "tclass" nameN;
 val (tyconN, tycon) = markup_string "tycon" nameN;
-val (fixed_declN, fixed_decl) = markup_string "fixed_decl" nameN;
 val (fixedN, fixed) = markup_string "fixed" nameN;
 val (constN, const) = markup_string "constant" nameN;
 val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Pure/General/markup.scala	Wed Apr 27 23:04:28 2011 +0200
@@ -149,7 +149,6 @@
 
   val TCLASS = "tclass"
   val TYCON = "tycon"
-  val FIXED_DECL = "fixed_decl"
   val FIXED = "fixed"
   val CONST = "constant"
   val DYNAMIC_FACT = "dynamic_fact"
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Pure/General/name_space.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -16,6 +16,7 @@
   val kind_of: T -> string
   val the_entry: T -> string ->
     {concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial}
+  val entry_ord: T -> string * string -> order
   val markup: T -> string -> Markup.T
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
@@ -125,9 +126,11 @@
     NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
   | SOME (_, entry) => entry);
 
+fun entry_ord space = int_ord o pairself (#id o the_entry space);
+
 fun markup (Name_Space {kind, entries, ...}) name =
   (case Symtab.lookup entries name of
-    NONE => Markup.malformed
+    NONE => Markup.hilite
   | SOME (_, entry) => entry_markup false kind (name, entry));
 
 fun is_concealed space name = #concealed (the_entry space name);
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -254,7 +254,7 @@
         thy
         |> Sign.declare_const_global ((b, ty0), syn)
         |> snd
-        |> pair ((Variable.name b, ty), (c, ty'))
+        |> pair ((Variable.check_name b, ty), (c, ty'))
       end;
   in
     thy
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Pure/Isar/element.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -99,7 +99,7 @@
 fun map_ctxt {binding, typ, term, pattern, fact, attrib} =
   fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx)))
    | Constrains xs => Constrains (xs |> map (fn (x, T) =>
-      (Variable.name (binding (Binding.name x)), typ T)))
+      (Variable.check_name (binding (Binding.name x)), typ T)))
    | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
       ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps)))))
    | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
@@ -222,9 +222,9 @@
 fun obtain prop ctxt =
   let
     val ((ps, prop'), ctxt') = Variable.focus prop ctxt;
-    fun fix (x, T) = (Binding.name (Proof_Context.revert_skolem ctxt' x), SOME T);
-    val xs = map (fix o Term.dest_Free o Thm.term_of o #2) ps;
-    val As = Logic.strip_imp_prems (Thm.term_of prop');
+    fun fix (x, T) = (Binding.name (Variable.revert_fixed ctxt' x), SOME T);
+    val xs = map (fix o #2) ps;
+    val As = Logic.strip_imp_prems prop';
   in ((Binding.empty, (xs, As)), ctxt') end;
 
 in
@@ -232,7 +232,6 @@
 fun pretty_statement ctxt kind raw_th =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val cert = Thm.cterm_of thy;
 
     val (th, is_elim) = standard_elim (Raw_Simplifier.norm_hhf raw_th);
     val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body true ctxt);
@@ -242,7 +241,7 @@
 
     val fixes = fold_aterms (fn v as Free (x, T) =>
         if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
-        then insert (op =) (Proof_Context.revert_skolem ctxt' x, T) else I | _ => I) prop [] |> rev;
+        then insert (op =) (Variable.revert_fixed ctxt' x, T) else I | _ => I) prop [] |> rev;
     val (assumes, cases) = take_suffix (fn prem =>
       is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
   in
@@ -250,7 +249,7 @@
     pretty_ctxt ctxt' (Assumes (map (fn t => (Attrib.empty_binding, [(t, [])])) assumes)) @
      (if null cases then pretty_stmt ctxt' (Shows [(Attrib.empty_binding, [(concl, [])])])
       else
-        let val (clauses, ctxt'') = fold_map (obtain o cert) cases ctxt'
+        let val (clauses, ctxt'') = fold_map obtain cases ctxt'
         in pretty_stmt ctxt'' (Obtains clauses) end)
   end |> thm_name kind raw_th;
 
@@ -526,7 +525,7 @@
 
 fun activate raw_elem ctxt =
   let val elem = raw_elem |> map_ctxt
-   {binding = tap Variable.name,
+   {binding = tap Variable.check_name,
     typ = I,
     term = I,
     pattern = I,
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Pure/Isar/expression.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -128,7 +128,7 @@
     val (implicit, expr') = params_expr expr;
 
     val implicit' = map #1 implicit;
-    val fixed' = map (Variable.name o #1) fixed;
+    val fixed' = map (Variable.check_name o #1) fixed;
     val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
     val implicit'' =
       if strict then []
@@ -393,7 +393,7 @@
     val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
 
     (* Retrieve parameter types *)
-    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.name o #1) fixes)
+    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.check_name o #1) fixes)
       | _ => fn ps => ps) (Fixes fors :: elems') [];
     val (Ts, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
     val parms = xs ~~ Ts;  (* params from expression and elements *)
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Pure/Isar/generic_target.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -67,12 +67,11 @@
     val mx' = check_mixfix lthy (b, extra_tfrees) mx;
 
     val type_params = map (Logic.mk_type o TFree) extra_tfrees;
+    val target_ctxt = Local_Theory.target_of lthy;
     val term_params =
-      rev (Variable.fixes_of (Local_Theory.target_of lthy))
-      |> map_filter (fn (_, x) =>
-        (case AList.lookup (op =) xs x of
-          SOME T => SOME (Free (x, T))
-        | NONE => NONE));
+      filter (Variable.is_fixed target_ctxt o #1) xs
+      |> sort (Variable.fixed_ord target_ctxt o pairself #1)
+      |> map Free;
     val params = type_params @ term_params;
 
     val U = map Term.fastype_of params ---> T;
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -632,7 +632,7 @@
 
 val case_spec =
   (Parse.$$$ "(" |--
-    Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.name) --| Parse.$$$ ")") ||
+    Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.binding) --| Parse.$$$ ")") ||
     Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> Parse.triple1;
 
 val _ =
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Pure/Isar/local_defs.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -8,7 +8,7 @@
 sig
   val cert_def: Proof.context -> term -> (string * typ) * term
   val abs_def: term -> (string * typ) * term
-  val mk_def: Proof.context -> (string * term) list -> term list
+  val mk_def: Proof.context -> (binding * term) list -> term list
   val expand: cterm list -> thm -> thm
   val def_export: Assumption.export
   val add_defs: ((binding * mixfix) * (Thm.binding * term)) list -> Proof.context ->
@@ -59,7 +59,7 @@
   let
     val (xs, rhss) = split_list args;
     val (bind, _) = Proof_Context.bind_fixes xs ctxt;
-    val lhss = map (fn (x, rhs) => bind (Free (x, Term.fastype_of rhs))) args;
+    val lhss = map (fn (x, rhs) => bind (Free (Binding.name_of x, Term.fastype_of rhs))) args;
   in map Logic.mk_equals (lhss ~~ rhss) end;
 
 
@@ -90,15 +90,14 @@
 
 fun add_defs defs ctxt =
   let
-    val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
+    val ((xs, mxs), specs) = defs |> split_list |>> split_list;
     val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
-    val xs = map Variable.name bvars;
-    val names = map2 Thm.def_binding_optional bvars bfacts;
+    val names = map2 Thm.def_binding_optional xs bfacts;
     val eqs = mk_def ctxt (xs ~~ rhss);
     val lhss = map (fst o Logic.dest_equals) eqs;
   in
     ctxt
-    |> Proof_Context.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
+    |> Proof_Context.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2
     |> fold Variable.declare_term eqs
     |> Proof_Context.add_assms_i def_export
       (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Pure/Isar/obtain.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -99,7 +99,7 @@
 
 fun bind_judgment ctxt name =
   let
-    val (bind, ctxt') = Proof_Context.bind_fixes [name] ctxt;
+    val (bind, ctxt') = Proof_Context.bind_fixes [Binding.name name] ctxt;
     val (t as _ $ Free v) = bind (Object_Logic.fixed_judgment (Proof_Context.theory_of ctxt) name);
   in ((v, t), ctxt') end;
 
@@ -118,25 +118,23 @@
 
     (*obtain vars*)
     val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
-    val (_, fix_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
-    val xs = map (Variable.name o #1) vars;
+    val (xs', fix_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
+    val xs = map (Variable.check_name o #1) vars;
 
     (*obtain asms*)
     val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
     val asm_props = maps (map fst) proppss;
     val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
 
-    val _ = Variable.warn_extra_tfrees fix_ctxt asms_ctxt;
+    (*obtain parms*)
+    val (Ts, parms_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt;
+    val parms = xs' ~~ Ts;
+    val _ = Variable.warn_extra_tfrees fix_ctxt parms_ctxt;
 
     (*obtain statements*)
     val thesisN = Name.variant xs Auto_Bind.thesisN;
     val (thesis_var, thesis) = #1 (bind_judgment fix_ctxt thesisN);
 
-    val asm_frees = fold Term.add_frees asm_props [];
-    val parms = xs |> map (fn x =>
-      let val x' = Proof_Context.get_skolem fix_ctxt x
-      in (x', the_default propT (AList.lookup (op =) asm_frees x')) end);
-
     val that_name = if name = "" then thatN else name;
     val that_prop =
       Term.list_all_free (parms, Logic.list_implies (asm_props, thesis))
@@ -198,7 +196,7 @@
     val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
     val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
     val obtain_rule = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule';
-    val ((params, stmt), fix_ctxt) = Variable.focus (Thm.cprem_of obtain_rule 1) ctxt';
+    val ((params, stmt), fix_ctxt) = Variable.focus_cterm (Thm.cprem_of obtain_rule 1) ctxt';
     val (prems, ctxt'') =
       Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params))
         (Drule.strip_imp_prems stmt) fix_ctxt;
@@ -257,7 +255,7 @@
 
 fun inferred_type (binding, _, mx) ctxt =
   let
-    val x = Variable.name binding;
+    val x = Variable.check_name binding;
     val (T, ctxt') = Proof_Context.inferred_param x ctxt
   in ((x, T, mx), ctxt') end;
 
@@ -280,7 +278,7 @@
       let
         val ((parms, rule), ctxt') =
           unify_params vars thesis_var raw_rule (Proof.context_of state');
-        val (bind, _) = Proof_Context.bind_fixes (map (#1 o #1) parms) ctxt';
+        val (bind, _) = Proof_Context.bind_fixes (map (Binding.name o #1 o #1) parms) ctxt';
         val ts = map (bind o Free o #1) parms;
         val ps = map dest_Free ts;
         val asms =
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -71,8 +71,8 @@
   val using_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
   val unfolding: ((thm list * attribute list) list) list -> state -> state
   val unfolding_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
-  val invoke_case: string * string option list * attribute list -> state -> state
-  val invoke_case_cmd: string * string option list * Attrib.src list -> state -> state
+  val invoke_case: string * binding option list * attribute list -> state -> state
+  val invoke_case_cmd: string * binding option list * Attrib.src list -> state -> state
   val begin_block: state -> state
   val next_block: state -> state
   val end_block: state -> state
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -63,8 +63,6 @@
   val cert_typ: Proof.context -> typ -> typ
   val cert_typ_syntax: Proof.context -> typ -> typ
   val cert_typ_abbrev: Proof.context -> typ -> typ
-  val get_skolem: Proof.context -> string -> string
-  val revert_skolem: Proof.context -> string -> string
   val infer_type: Proof.context -> string * typ -> typ
   val inferred_param: string -> Proof.context -> typ * Proof.context
   val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
@@ -127,7 +125,7 @@
   val add_fixes: (binding * typ option * mixfix) list -> Proof.context ->
     string list * Proof.context
   val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
-  val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context
+  val bind_fixes: binding list -> Proof.context -> (term -> term) * Proof.context
   val add_assms: Assumption.export ->
     (Thm.binding * (string * string list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
@@ -136,7 +134,7 @@
     Proof.context -> (string * thm list) list * Proof.context
   val add_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
   val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
-  val get_case: Proof.context -> string -> string option list -> Rule_Cases.T
+  val get_case: Proof.context -> string -> binding option list -> Rule_Cases.T
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
   val target_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
@@ -408,10 +406,7 @@
 
 (** prepare variables **)
 
-(* internalize Skolem constants *)
-
-val lookup_skolem = AList.lookup (op =) o Variable.fixes_of;
-fun get_skolem ctxt x = the_default x (lookup_skolem ctxt x);
+(* check Skolem constants *)
 
 fun no_skolem internal x =
   if can Name.dest_skolem x then
@@ -421,14 +416,6 @@
   else x;
 
 
-(* revert Skolem constants -- if possible *)
-
-fun revert_skolem ctxt x =
-  (case find_first (fn (_, y) => y = x) (Variable.fixes_of ctxt) of
-    SOME (x', _) => if lookup_skolem ctxt x' = SOME x then x' else x
-  | NONE => x);
-
-
 
 (** prepare terms and propositions **)
 
@@ -443,7 +430,7 @@
 
 fun inferred_fixes ctxt =
   let
-    val xs = rev (map #2 (Variable.fixes_of ctxt));
+    val xs = map #2 (Variable.dest_fixes ctxt);
     val (Ts, ctxt') = fold_map inferred_param xs ctxt;
   in (xs ~~ Ts, ctxt') end;
 
@@ -508,7 +495,7 @@
     val (c, pos) = token_content text;
     val _ = no_skolem false c;
   in
-    (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
+    (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
       (SOME x, false) =>
         (Context_Position.report ctxt pos
             (Markup.name x (if can Name.dest_skolem x then Markup.skolem else Markup.free));
@@ -524,7 +511,7 @@
 fun intern_skolem ctxt x =
   let
     val _ = no_skolem false x;
-    val sko = lookup_skolem ctxt x;
+    val sko = Variable.lookup_fixed ctxt x;
     val is_const = can (read_const_proper ctxt false) x orelse Long_Name.is_qualified x;
     val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
   in
@@ -941,7 +928,7 @@
 fun prep_vars prep_typ internal =
   fold_map (fn (b, raw_T, mx) => fn ctxt =>
     let
-      val x = Variable.name b;
+      val x = Variable.check_name b;
       val _ = Lexicon.is_identifier (no_skolem internal x) orelse
         error ("Illegal variable name: " ^ Binding.print b);
 
@@ -1040,15 +1027,16 @@
 
 fun add_fixes raw_vars ctxt =
   let
-    val (vars, _) = cert_vars raw_vars ctxt;
-    val (xs', ctxt') = Variable.add_fixes (map (Variable.name o #1) vars) ctxt;
-    val ctxt'' =
-      ctxt'
-      |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
-      |-> (map_syntax o Local_Syntax.add_syntax (theory_of ctxt) o map (pair Local_Syntax.Fixed));
-    val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
-      Context_Position.report ctxt (Binding.pos_of b) (Markup.fixed_decl x'));
-  in (xs', ctxt'') end;
+    val thy = theory_of ctxt;
+    val vars = #1 (cert_vars raw_vars ctxt);
+  in
+    ctxt
+    |> Variable.add_fixes_binding (map #1 vars)
+    |-> (fn xs =>
+      fold_map declare_var (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
+      #-> (map_syntax o Local_Syntax.add_syntax thy o map (pair Local_Syntax.Fixed))
+      #> pair xs)
+  end;
 
 
 (* fixes vs. frees *)
@@ -1056,12 +1044,13 @@
 fun auto_fixes (ctxt, (propss, x)) =
   ((fold o fold) Variable.auto_fixes propss ctxt, (propss, x));
 
-fun bind_fixes xs ctxt =
+fun bind_fixes bs ctxt =
   let
-    val (_, ctxt') = ctxt |> add_fixes (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
+    val (_, ctxt') = ctxt |> add_fixes (map (fn b => (b, NONE, NoSyn)) bs);
+    val xs = map Binding.name_of bs;
     fun bind (t as Free (x, T)) =
           if member (op =) xs x then
-            (case lookup_skolem ctxt' x of SOME x' => Free (x', T) | NONE => t)
+            (case Variable.lookup_fixed ctxt' x of SOME x' => Free (x', T) | NONE => t)
           else t
       | bind (t $ u) = bind t $ bind u
       | bind (Abs (x, T, t)) = Abs (x, T, bind t)
@@ -1123,7 +1112,7 @@
 fun fix (x, T) ctxt =
   let
     val (bind, ctxt') = bind_fixes [x] ctxt;
-    val t = bind (Free (x, T));
+    val t = bind (Free (Binding.name_of x, T));
   in (t, ctxt' |> Variable.declare_constraints t) end;
 
 in
@@ -1233,7 +1222,7 @@
   in
     Pretty.block (Pretty.fbreaks
       (Pretty.str (name ^ ":") ::
-        prt_sect "fix" [] (Pretty.str o fst) fixes @
+        prt_sect "fix" [] (Pretty.str o Binding.name_of o fst) fixes @
         prt_sect "let" [Pretty.str "and"] prt_let
           (map_filter (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @
         (if forall (null o #2) asms then []
@@ -1282,8 +1271,8 @@
         if x = x' then Pretty.str x
         else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')];
       val fixes =
-        rev (filter_out ((can Name.dest_internal orf member (op =) structs) o #1)
-          (Variable.fixes_of ctxt));
+        filter_out ((can Name.dest_internal orf member (op =) structs) o #1)
+          (Variable.dest_fixes ctxt);
       val prt_fixes =
         if null fixes then []
         else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -20,7 +20,7 @@
 sig
   include BASIC_RULE_CASES
   datatype T = Case of
-   {fixes: (string * typ) list,
+   {fixes: (binding * typ) list,
     assumes: (string * term list) list,
     binds: (indexname * term option) list,
     cases: (string * T) list}
@@ -56,7 +56,7 @@
 (** cases **)
 
 datatype T = Case of
- {fixes: (string * typ) list,
+ {fixes: (binding * typ) list,
   assumes: (string * term list) list,
   binds: (indexname * term option) list,
   cases: (string * T) list};
@@ -93,6 +93,8 @@
         chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
       in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end;
 
+fun bindings args = map (apfst Binding.name) args;
+
 fun extract_case thy (case_outline, raw_prop) name concls =
   let
     val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
@@ -122,11 +124,12 @@
     val cases = map extract props;
 
     fun common_case ((fixes1, assumes1), ((fixes2, assumes2), binds)) =
-      Case {fixes = fixes1 @ fixes2, assumes = assumes1 @ assumes2, binds = binds, cases = []};
+      Case {fixes = bindings (fixes1 @ fixes2),
+        assumes = assumes1 @ assumes2, binds = binds, cases = []};
     fun inner_case (_, ((fixes2, assumes2), binds)) =
-      Case {fixes = fixes2, assumes = assumes2, binds = binds, cases = []};
+      Case {fixes = bindings fixes2, assumes = assumes2, binds = binds, cases = []};
     fun nested_case ((fixes1, assumes1), _) =
-      Case {fixes = fixes1, assumes = assumes1, binds = [],
+      Case {fixes = bindings fixes1, assumes = assumes1, binds = [],
         cases = map string_of_int (1 upto len) ~~ map inner_case cases};
   in
     if len = 0 then NONE
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Pure/Isar/specification.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -169,7 +169,7 @@
 fun gen_axioms do_print prep raw_vars raw_specs thy =
   let
     val ((vars, specs), _) = prep raw_vars raw_specs (Proof_Context.init_global thy);
-    val xs = map (fn ((b, T), _) => (Variable.name b, T)) vars;
+    val xs = map (fn ((b, T), _) => (Variable.check_name b, T)) vars;
 
     (*consts*)
     val (consts, consts_thy) = thy |> fold_map Theory.specify_const vars;
@@ -179,7 +179,7 @@
     val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
         fold_map Thm.add_axiom_global
           (map (apfst (fn a => Binding.map_name (K a) b))
-            (Global_Theory.name_multi (Variable.name b) (map subst props)))
+            (Global_Theory.name_multi (Variable.check_name b) (map subst props)))
         #>> (fn ths => ((b, atts), [(map #2 ths, [])])));
 
     (*facts*)
@@ -211,7 +211,7 @@
         [] => (Binding.name x, NoSyn)
       | [((b, _), mx)] =>
           let
-            val y = Variable.name b;
+            val y = Variable.check_name b;
             val _ = x = y orelse
               error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
                 Position.str_of (Binding.pos_of b));
@@ -250,7 +250,7 @@
         [] => (Binding.name x, NoSyn)
       | [((b, _), mx)] =>
           let
-            val y = Variable.name b;
+            val y = Variable.check_name b;
             val _ = x = y orelse
               error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
                 Position.str_of (Binding.pos_of b));
@@ -320,10 +320,10 @@
   | Element.Obtains obtains =>
       let
         val case_names = obtains |> map_index (fn (i, (b, _)) =>
-          if Binding.is_empty b then string_of_int (i + 1) else Variable.name b);
+          if Binding.is_empty b then string_of_int (i + 1) else Variable.check_name b);
         val constraints = obtains |> map (fn (_, (vars, _)) =>
           Element.Constrains
-            (vars |> map_filter (fn (x, SOME T) => SOME (Variable.name x, T) | _ => NONE)));
+            (vars |> map_filter (fn (x, SOME T) => SOME (Variable.check_name x, T) | _ => NONE)));
 
         val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
         val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
@@ -333,7 +333,7 @@
         fun assume_case ((name, (vars, _)), asms) ctxt' =
           let
             val bs = map fst vars;
-            val xs = map Variable.name bs;
+            val xs = map Variable.check_name bs;
             val props = map fst asms;
             val (Ts, _) = ctxt'
               |> fold Variable.declare_term props
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -31,8 +31,9 @@
 
 fun markup_free ctxt x =
   [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
-  (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then []
-   else [Markup.hilite]);
+  (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
+   then [Variable.markup_fixed ctxt x]
+   else []);
 
 fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
 
@@ -592,7 +593,7 @@
       else Markup.hilite;
   in
     if can Name.dest_skolem x
-    then ([m, Markup.skolem], Proof_Context.revert_skolem ctxt x)
+    then ([m, Markup.skolem], Variable.revert_fixed ctxt x)
     else ([m, Markup.free], x)
   end;
 
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/conv.ML
--- a/src/Pure/conv.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Pure/conv.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -93,7 +93,7 @@
   (case Thm.term_of ct of
     Abs (x, _, _) =>
       let
-        val ([u], ctxt') = Variable.variant_fixes ["u"] ctxt;
+        val (u, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt;
         val (v, ct') = Thm.dest_abs (SOME u) ct;
         val eq = cv (v, ctxt') ct';
       in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Pure/goal.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -326,7 +326,7 @@
 
 fun assume_rule_tac ctxt = norm_hhf_tac THEN' CSUBGOAL (fn (goal, i) =>
   let
-    val ((_, goal'), ctxt') = Variable.focus goal ctxt;
+    val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
     val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
     val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
     val tacs = Rs |> map (fn R =>
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Pure/subgoal.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -33,7 +33,7 @@
   let
     val st = Simplifier.norm_hhf_protect raw_st;
     val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
-    val ((params, goal), ctxt2) = Variable.focus (Thm.cprem_of st' i) ctxt1;
+    val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
 
     val (asms, concl) =
       if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Pure/variable.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -10,15 +10,12 @@
   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 check_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
@@ -35,14 +32,23 @@
   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 is_fixed: Proof.context -> string -> bool
+  val newly_fixed: Proof.context -> Proof.context -> string -> bool
+  val fixed_ord: Proof.context -> string * string -> order
+  val intern_fixed: Proof.context -> string -> string
+  val markup_fixed: Proof.context -> string -> Markup.T
+  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
@@ -61,7 +67,8 @@
     (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context
   val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
-  val focus: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
+  val focus: term -> Proof.context -> ((string * (string * typ)) list * term) * Proof.context
+  val focus_cterm: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
   val focus_subgoal: int -> thm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
   val warn_extra_tfrees: Proof.context -> Proof.context -> unit
   val polymorphic_types: Proof.context -> term list -> (indexname * sort) list * term list
@@ -73,11 +80,14 @@
 
 (** 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*)
@@ -94,8 +104,8 @@
 (
   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 =
@@ -146,6 +156,7 @@
 
 val names_of = #names o rep_data;
 val fixes_of = #fixes o rep_data;
+val fixes_space = #1 o fixes_of;
 val binds_of = #binds o rep_data;
 val type_occs_of = #type_occs o rep_data;
 val maxidx_of = #maxidx o rep_data;
@@ -153,11 +164,8 @@
 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;
+val check_name = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming;
 
 
 
@@ -281,6 +289,29 @@
 
 (** fixes **)
 
+(* specialized name space *)
+
+fun is_fixed ctxt x = can (Name_Space.the_entry (fixes_space ctxt)) x;
+fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);
+
+val fixed_ord = Name_Space.entry_ord o fixes_space;
+val intern_fixed = Name_Space.intern o fixes_space;
+val markup_fixed = Name_Space.markup o fixes_space;
+
+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 =
@@ -300,41 +331,54 @@
 
 local
 
-fun no_dups [] = ()
-  | no_dups dups = error ("Duplicate fixed variable(s): " ^ commas_quote dups);
+fun err_dups dups =
+  error ("Duplicate fixed variable(s): " ^ commas (map Binding.print dups));
 
-fun new_fixes names' xs xs' =
+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 check_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
@@ -358,10 +402,10 @@
 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;
@@ -473,23 +517,34 @@
 val trade = gen_trade (import true) export;
 
 
-(* focus on outermost parameters *)
+(* focus on outermost parameters: !!x y z. B *)
+
+fun focus_params t ctxt =
+  let
+    val (xs, Ts) =
+      split_list (Term.variant_frees t (Term.strip_all_vars t));  (*as they are printed :-*)
+    val (xs', ctxt') = variant_fixes xs ctxt;
+    val ps = xs' ~~ Ts;
+    val ctxt'' = ctxt' |> fold (declare_constraints o Free) ps;
+  in ((xs, ps), ctxt'') end;
+
+fun focus t ctxt =
+  let
+    val ((xs, ps), ctxt') = focus_params t ctxt;
+    val t' = Term.subst_bounds (rev (map Free ps), Term.strip_all_body t);
+  in (((xs ~~ ps), t'), ctxt') end;
 
 fun forall_elim_prop t prop =
   Thm.beta_conversion false (Thm.capply (Thm.dest_arg prop) t)
   |> Thm.cprop_of |> Thm.dest_arg;
 
-fun focus goal ctxt =
+fun focus_cterm goal ctxt =
   let
     val cert = Thm.cterm_of (Thm.theory_of_cterm goal);
-    val t = Thm.term_of goal;
-    val ps = Term.variant_frees t (Term.strip_all_vars t);   (*as they are printed :-*)
-    val (xs, Ts) = split_list ps;
-    val (xs', ctxt') = variant_fixes xs ctxt;
-    val ps' = ListPair.map (cert o Free) (xs', Ts);
+    val ((xs, ps), ctxt') = focus_params (Thm.term_of goal) ctxt;
+    val ps' = map (cert o Free) ps;
     val goal' = fold forall_elim_prop ps' goal;
-    val ctxt'' = ctxt' |> fold (declare_constraints o Thm.term_of) ps';
-  in ((xs ~~ ps', goal'), ctxt'') end;
+  in ((xs ~~ ps', goal'), ctxt') end;
 
 fun focus_subgoal i st =
   let
@@ -498,7 +553,7 @@
   in
     fold bind_term no_binds #>
     fold (declare_constraints o Var) all_vars #>
-    focus (Thm.cprem_of st i)
+    focus_cterm (Thm.cprem_of st i)
   end;
 
 
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Tools/coherent.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -213,7 +213,7 @@
   SUBPROOF (fn {prems = prems', concl, context, ...} =>
     let val xs = map (term_of o #2) params @
       map (fn (_, s) => Free (s, the (Variable.default_type context s)))
-        (Variable.fixes_of context)
+        (rev (Variable.dest_fixes context))  (* FIXME !? *)
     in
       case valid context (map mk_rule (prems' @ prems @ rules)) (term_of concl)
            (mk_dom xs) Net.empty 0 0 of
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Tools/induct.ML	Wed Apr 27 23:04:28 2011 +0200
@@ -599,7 +599,7 @@
 
 fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] =
       let
-        val x = Name.clean (Proof_Context.revert_skolem ctxt z);
+        val x = Name.clean (Variable.revert_fixed ctxt z);
         fun index i [] = []
           | index i (y :: ys) =
               if x = y then x ^ string_of_int i :: index (i + 1) ys
@@ -646,7 +646,7 @@
     val v = Free (x, T);
     fun spec_rule prfx (xs, body) =
       @{thm Pure.meta_spec}
-      |> Thm.rename_params_rule ([Name.clean (Proof_Context.revert_skolem ctxt x)], 1)
+      |> Thm.rename_params_rule ([Name.clean (Variable.revert_fixed ctxt x)], 1)
       |> Thm.lift_rule (cert prfx)
       |> `(Thm.prop_of #> Logic.strip_assums_concl)
       |-> (fn pred $ arg =>
diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Tools/jEdit/src/jedit/isabelle_markup.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Wed Apr 27 21:17:47 2011 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Wed Apr 27 23:04:28 2011 +0200
@@ -152,7 +152,6 @@
       // logical entities
       Markup.TCLASS -> NULL,
       Markup.TYCON -> NULL,
-      Markup.FIXED_DECL -> FUNCTION,
       Markup.FIXED -> NULL,
       Markup.CONST -> LITERAL2,
       Markup.DYNAMIC_FACT -> LABEL,