clarified standardization of variables, with proper treatment of local variables;
tuned signature;
tuned;

--- a/src/Pure/Thy/export_theory.ML	Wed Sep 19 22:18:36 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Thu Sep 20 22:39:39 2018 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Thy/export_theory.ML
     Author:     Makarius
 
-Export foundational theory content.
+Export foundational theory content and locale/class structure.
 *)
 
 signature EXPORT_THEORY =
@@ -13,28 +13,63 @@
 structure Export_Theory: EXPORT_THEORY =
 struct
 
-(* names for bound variables *)
+(* standardization of variables: only frees and named bounds *)
 
 local
-  fun declare_names (Abs (_, _, b)) = declare_names b
-    | declare_names (t $ u) = declare_names t #> declare_names u
-    | declare_names (Const (c, _)) = Name.declare (Long_Name.base_name c)
-    | declare_names (Free (x, _)) = Name.declare x
-    | declare_names _ = I;
+
+fun declare_names (Abs (_, _, b)) = declare_names b
+  | declare_names (t $ u) = declare_names t #> declare_names u
+  | declare_names (Const (c, _)) = Name.declare (Long_Name.base_name c)
+  | declare_names (Free (x, _)) = Name.declare x
+  | declare_names _ = I;
+
+fun variant_abs bs (Abs (x, T, t)) =
+      let
+        val names = fold Name.declare bs (declare_names t Name.context);
+        val x' = #1 (Name.variant x names);
+        val t' = variant_abs (x' :: bs) t;
+      in Abs (x', T, t') end
+  | variant_abs bs (t $ u) = variant_abs bs t $ variant_abs bs u
+  | variant_abs _ t = t;
+
+in
+
+fun standard_vars used =
+  let
+    fun zero_var_indexes tm =
+      Term_Subst.instantiate (Term_Subst.zero_var_indexes_inst used [tm]) tm;
 
-  fun variant_abs bs (Abs (x, T, t)) =
-        let
-          val names = fold Name.declare bs (declare_names t Name.context);
-          val x' = #1 (Name.variant x names);
-          val t' = variant_abs (x' :: bs) t;
-        in Abs (x', T, t') end
-    | variant_abs bs (t $ u) = variant_abs bs t $ variant_abs bs u
-    | variant_abs _ t = t;
-in
-  val named_bounds = variant_abs [];
+    fun unvarifyT ty = ty |> Term.map_atyps
+      (fn TVar ((a, _), S) => TFree (a, S)
+        | T as TFree (a, _) =>
+            if Name.is_declared used a then T
+            else raise TYPE (Logic.bad_fixed a, [ty], []));
+
+    fun unvarify tm = tm |> Term.map_aterms
+      (fn Var ((x, _), T) => Free (x, T)
+        | t as Free (x, _) =>
+            if Name.is_declared used x then t
+            else raise TERM (Logic.bad_fixed x, [tm])
+        | t => t);
+
+  in zero_var_indexes #> map_types unvarifyT #> unvarify #> variant_abs [] end;
+
+val standard_vars_global = standard_vars Name.context;
+
 end;
 
 
+(* free variables: not declared in the context *)
+
+val is_free = not oo Name.is_declared;
+
+fun add_frees used =
+  fold_aterms (fn Free (x, T) => is_free used x ? insert (op =) (x, T) | _ => I);
+
+fun add_tfrees used =
+  (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I);
+
+
 (* locale support *)
 
 fun locale_axioms thy loc =
@@ -141,55 +176,58 @@
     (* consts *)
 
     val encode_const =
-      let open XML.Encode Term_XML.Encode in
-        pair (option encode_infix) (pair (list string) (pair typ (option (term o named_bounds))))
-      end;
+      let open XML.Encode Term_XML.Encode
+      in pair (option encode_infix) (pair (list string) (pair typ (option term))) end;
 
     fun export_const c (T, abbrev) =
       let
         val syntax = get_infix_const thy_ctxt c;
         val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
-        val abbrev' = abbrev |> Option.map (Logic.unvarify_global #> map_types Type.strip_sorts);
+        val abbrev' = abbrev |> Option.map (standard_vars_global #> map_types Type.strip_sorts);
         val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
-      in SOME (encode_const (syntax, (args, (T', abbrev')))) end;
+      in encode_const (syntax, (args, (T', abbrev'))) end;
 
     val _ =
-      export_entities "consts" export_const Sign.const_space
+      export_entities "consts" (SOME oo export_const) Sign.const_space
         (#constants (Consts.dest (Sign.consts_of thy)));
 
 
     (* axioms and facts *)
 
-    fun standard_prop_of raw_thm =
+    fun prop_of raw_thm =
       let
         val thm = raw_thm
           |> Thm.transfer thy
           |> Thm.check_hyps (Context.Theory thy)
           |> Thm.strip_shyps;
         val prop = thm
-          |> Thm.full_prop_of
-          |> Term_Subst.zero_var_indexes;
+          |> Thm.full_prop_of;
       in (Thm.extra_shyps thm, prop) end;
 
-    fun encode_prop (Ss, prop) =
+    fun encode_prop used (Ss, raw_prop) =
       let
-        val prop' = Logic.unvarify_global (named_bounds prop);
-        val typargs = rev (Term.add_tfrees prop' []);
-        val sorts = Name.invent (Name.make_context (map #1 typargs)) Name.aT (length Ss) ~~ Ss;
-        val args = rev (Term.add_frees prop' []);
+        val prop = standard_vars used raw_prop;
+        val args = rev (add_frees used prop []);
+        val typargs = rev (add_tfrees used prop []);
+        val used' = fold (Name.declare o #1) typargs used;
+        val sorts = Name.invent used' Name.aT (length Ss) ~~ Ss;
       in
-        (sorts @ typargs, args, prop') |>
+        (sorts @ typargs, args, prop) |>
           let open XML.Encode Term_XML.Encode
           in triple (list (pair string sort)) (list (pair string typ)) term end
       end;
 
-    val encode_fact = XML.Encode.list encode_prop o map standard_prop_of;
+    fun encode_axiom used t = encode_prop used ([], t);
+
+    val encode_fact_single = encode_prop Name.context o prop_of;
+    val encode_fact_multi = XML.Encode.list (encode_prop Name.context) o map prop_of;
 
     val _ =
-      export_entities "axioms" (fn _ => fn t => SOME (encode_prop ([], t))) Theory.axiom_space
-        (Theory.axioms_of thy);
+      export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t))
+        Theory.axiom_space (Theory.axioms_of thy);
     val _ =
-      export_entities "facts" (K (SOME o encode_fact)) (Facts.space_of o Global_Theory.facts_of)
+      export_entities "facts" (K (SOME o encode_fact_multi))
+        (Facts.space_of o Global_Theory.facts_of)
         (Facts.dest_static true [] (Global_Theory.facts_of thy));
 
 
@@ -197,13 +235,12 @@
 
     val encode_class =
       let open XML.Encode Term_XML.Encode
-      in pair (list (pair string typ)) (list (term o named_bounds)) end;
+      in pair (list (pair string typ)) (list encode_fact_single) end;
 
     fun export_class name =
       (case try (Axclass.get_info thy) name of
         NONE => ([], [])
-      | SOME {params, axioms, ...} =>
-          (params, map (Logic.unvarify_global o Thm.full_prop_of) axioms))
+      | SOME {params, axioms, ...} => (params, axioms))
       |> encode_class |> SOME;
 
     val _ =
@@ -231,18 +268,20 @@
 
     (* locales *)
 
-    fun encode_locale loc ({type_params, params, ...}: Locale.content) =
+    fun encode_locale used =
+      let open XML.Encode Term_XML.Encode
+      in triple (list (pair string sort)) (list (pair string typ)) (list (encode_axiom used)) end;
+
+    fun export_locale loc ({type_params, params, ...}: Locale.content) =
       let
         val axioms = locale_axioms thy loc;
         val args = map #1 params;
-        val typargs = type_params @ rev (fold Term.add_tfrees (map Free args @ axioms) []);
-        val encode =
-          let open XML.Encode Term_XML.Encode
-          in triple (list (pair string sort)) (list (pair string typ)) (list term) end;
-      in encode (typargs, args, axioms) end;
+        val typargs = rev (fold Term.add_tfrees (map Free args @ axioms) (rev type_params));
+        val used = fold Name.declare (map #1 typargs @ map #1 args) Name.context;
+      in encode_locale used (typargs, args, axioms) end;
 
     val _ =
-      export_entities "locales" (SOME oo encode_locale) Locale.locale_space
+      export_entities "locales" (SOME oo export_locale) Locale.locale_space
         (Locale.dest_locales thy);
 
 

--- a/src/Pure/Thy/export_theory.scala	Wed Sep 19 22:18:36 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Thu Sep 20 22:39:39 2018 +0200
@@ -328,12 +328,12 @@
   /* type classes */
 
   sealed case class Class(
-    entity: Entity, params: List[(String, Term.Typ)], axioms: List[Term.Term])
+    entity: Entity, params: List[(String, Term.Typ)], axioms: List[Prop])
   {
     def cache(cache: Term.Cache): Class =
       Class(entity.cache(cache),
         params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
-        axioms.map(cache.term(_)))
+        axioms.map(_.cache(cache)))
   }
 
   def read_classes(provider: Export.Provider): List[Class] =
@@ -344,7 +344,7 @@
         {
           import XML.Decode._
           import Term_XML.Decode._
-          pair(list(pair(string, typ)), list(term))(body)
+          pair(list(pair(string, typ)), list(decode_prop))(body)
         }
         Class(entity, params, axioms)
       })
@@ -356,13 +356,13 @@
     entity: Entity,
     typargs: List[(String, Term.Sort)],
     args: List[(String, Term.Typ)],
-    axioms: List[Term.Term])
+    axioms: List[Prop])
   {
     def cache(cache: Term.Cache): Locale =
       Locale(entity.cache(cache),
         typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
         args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
-        axioms.map(cache.term(_)))
+        axioms.map(_.cache(cache)))
   }
 
   def read_locales(provider: Export.Provider): List[Locale] =
@@ -373,7 +373,7 @@
         {
           import XML.Decode._
           import Term_XML.Decode._
-          triple(list(pair(string, sort)), list(pair(string, typ)), list(term))(body)
+          triple(list(pair(string, sort)), list(pair(string, typ)), list(decode_prop))(body)
         }
         Locale(entity, typargs, args, axioms)
       })

--- a/src/Pure/drule.ML	Wed Sep 19 22:18:36 2018 +0200
+++ b/src/Pure/drule.ML	Thu Sep 20 22:39:39 2018 +0200
@@ -220,7 +220,8 @@
 fun zero_var_indexes_list [] = []
   | zero_var_indexes_list ths =
       let
-        val (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths);
+        val (instT, inst) =
+          Term_Subst.zero_var_indexes_inst Name.context (map Thm.full_prop_of ths);
 
         val tvars = fold Thm.add_tvars ths [];
         fun the_tvar v = the (find_first (fn cT => v = dest_TVar (Thm.typ_of cT)) tvars);

--- a/src/Pure/logic.ML	Wed Sep 19 22:18:36 2018 +0200
+++ b/src/Pure/logic.ML	Thu Sep 20 22:39:39 2018 +0200
@@ -80,6 +80,8 @@
   val list_rename_params: string list -> term -> term
   val assum_pairs: int * term -> (term * term) list
   val assum_problems: int * term -> (term -> term) * term list * term
+  val bad_schematic: indexname -> string
+  val bad_fixed: string -> string
   val varifyT_global: typ -> typ
   val unvarifyT_global: typ -> typ
   val varify_types_global: term -> term

--- a/src/Pure/term_subst.ML	Wed Sep 19 22:18:36 2018 +0200
+++ b/src/Pure/term_subst.ML	Thu Sep 20 22:39:39 2018 +0200
@@ -29,7 +29,7 @@
   val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
   val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
     term -> term
-  val zero_var_indexes_inst: term list ->
+  val zero_var_indexes_inst: Name.context -> term list ->
     ((indexname * sort) * typ) list * ((indexname * typ) * term) list
   val zero_var_indexes: term -> term
   val zero_var_indexes_list: term list -> term list
@@ -211,21 +211,21 @@
     val (x', used') = Name.variant (if Name.is_bound x then "u" else x) used;
   in if x = x' andalso i = 0 then (inst, used') else ((v, mk ((x', 0), X)) :: inst, used') end;
 
-fun zero_var_indexes_inst ts =
+fun zero_var_indexes_inst used ts =
   let
     val (instT, _) =
       TVars.fold (zero_var_inst TVar o #1)
         ((fold o fold_types o fold_atyps) (fn TVar v =>
           TVars.insert (K true) (v, ()) | _ => I) ts TVars.empty)
-        ([], Name.context);
+        ([], used);
     val (inst, _) =
       Vars.fold (zero_var_inst Var o #1)
         ((fold o fold_aterms) (fn Var (xi, T) =>
           Vars.insert (K true) ((xi, instantiateT instT T), ()) | _ => I) ts Vars.empty)
-        ([], Name.context);
+        ([], used);
   in (instT, inst) end;
 
-fun zero_var_indexes_list ts = map (instantiate (zero_var_indexes_inst ts)) ts;
+fun zero_var_indexes_list ts = map (instantiate (zero_var_indexes_inst Name.context ts)) ts;
 val zero_var_indexes = singleton zero_var_indexes_list;
 
 end;