src/Pure/Thy/export_theory.ML
changeset 70529 2ecbbe6b35db
parent 70386 6af87375b95f
child 70534 fb876ebbf5a7
     1.1 --- a/src/Pure/Thy/export_theory.ML	Wed Aug 14 11:14:27 2019 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Wed Aug 14 19:21:34 2019 +0200
     1.3 @@ -44,52 +44,6 @@
     1.4        in ([], triple int string int (ass, delim, pri)) end];
     1.5  
     1.6  
     1.7 -(* standardization of variables: only frees and named bounds *)
     1.8 -
     1.9 -local
    1.10 -
    1.11 -fun declare_names (Abs (_, _, b)) = declare_names b
    1.12 -  | declare_names (t $ u) = declare_names t #> declare_names u
    1.13 -  | declare_names (Const (c, _)) = Name.declare (Long_Name.base_name c)
    1.14 -  | declare_names (Free (x, _)) = Name.declare x
    1.15 -  | declare_names _ = I;
    1.16 -
    1.17 -fun variant_abs bs (Abs (x, T, t)) =
    1.18 -      let
    1.19 -        val names = fold Name.declare bs (declare_names t Name.context);
    1.20 -        val x' = #1 (Name.variant x names);
    1.21 -        val t' = variant_abs (x' :: bs) t;
    1.22 -      in Abs (x', T, t') end
    1.23 -  | variant_abs bs (t $ u) = variant_abs bs t $ variant_abs bs u
    1.24 -  | variant_abs _ t = t;
    1.25 -
    1.26 -in
    1.27 -
    1.28 -fun standard_vars used =
    1.29 -  let
    1.30 -    fun zero_var_indexes tm =
    1.31 -      Term_Subst.instantiate (Term_Subst.zero_var_indexes_inst used [tm]) tm;
    1.32 -
    1.33 -    fun unvarifyT ty = ty |> Term.map_atyps
    1.34 -      (fn TVar ((a, _), S) => TFree (a, S)
    1.35 -        | T as TFree (a, _) =>
    1.36 -            if Name.is_declared used a then T
    1.37 -            else raise TYPE (Logic.bad_fixed a, [ty], []));
    1.38 -
    1.39 -    fun unvarify tm = tm |> Term.map_aterms
    1.40 -      (fn Var ((x, _), T) => Free (x, T)
    1.41 -        | t as Free (x, _) =>
    1.42 -            if Name.is_declared used x then t
    1.43 -            else raise TERM (Logic.bad_fixed x, [tm])
    1.44 -        | t => t);
    1.45 -
    1.46 -  in zero_var_indexes #> map_types unvarifyT #> unvarify #> variant_abs [] end;
    1.47 -
    1.48 -val standard_vars_global = standard_vars Name.context;
    1.49 -
    1.50 -end;
    1.51 -
    1.52 -
    1.53  (* free variables: not declared in the context *)
    1.54  
    1.55  val is_free = not oo Name.is_declared;
    1.56 @@ -253,7 +207,8 @@
    1.57          val U = Logic.unvarifyT_global T;
    1.58          val U0 = Type.strip_sorts U;
    1.59          val recursion = primrec_types thy_ctxt (c, U);
    1.60 -        val abbrev' = abbrev |> Option.map (standard_vars_global #> map_types Type.strip_sorts);
    1.61 +        val abbrev' = abbrev
    1.62 +          |> Option.map (Proofterm.standard_vars_term Name.context #> map_types Type.strip_sorts);
    1.63          val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, U0));
    1.64          val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0);
    1.65        in encode_const (syntax, (args, (U0, (abbrev', (propositional, recursion))))) end;
    1.66 @@ -277,7 +232,7 @@
    1.67  
    1.68      fun encode_prop used (Ss, raw_prop) =
    1.69        let
    1.70 -        val prop = standard_vars used raw_prop;
    1.71 +        val prop = Proofterm.standard_vars_term used raw_prop;
    1.72          val args = rev (add_frees used prop []);
    1.73          val typargs = rev (add_tfrees used prop []);
    1.74          val used' = fold (Name.declare o #1) typargs used;