src/Pure/Thy/export_theory.ML

--- a/src/Pure/Thy/export_theory.ML	Wed Aug 14 11:14:27 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Wed Aug 14 19:21:34 2019 +0200
@@ -44,52 +44,6 @@
       in ([], triple int string int (ass, delim, pri)) end];
 
 
-(* 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 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 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;
@@ -253,7 +207,8 @@
         val U = Logic.unvarifyT_global T;
         val U0 = Type.strip_sorts U;
         val recursion = primrec_types thy_ctxt (c, U);
-        val abbrev' = abbrev |> Option.map (standard_vars_global #> map_types Type.strip_sorts);
+        val abbrev' = abbrev
+          |> Option.map (Proofterm.standard_vars_term Name.context #> map_types Type.strip_sorts);
         val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, U0));
         val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0);
       in encode_const (syntax, (args, (U0, (abbrev', (propositional, recursion))))) end;
@@ -277,7 +232,7 @@
 
     fun encode_prop used (Ss, raw_prop) =
       let
-        val prop = standard_vars used raw_prop;
+        val prop = Proofterm.standard_vars_term 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;