explicit names for bound variables;
authorwenzelm
Sun Aug 05 14:50:11 2018 +0200 (11 months ago)
changeset 68725367e60d9aa1b
parent 68724 7fafadbf16c7
child 68726 782d6b89fb19
explicit names for bound variables;
src/Pure/Thy/export_theory.ML
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sat Aug 04 22:32:41 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sun Aug 05 14:50:11 2018 +0200
     1.3 @@ -13,6 +13,28 @@
     1.4  structure Export_Theory: EXPORT_THEORY =
     1.5  struct
     1.6  
     1.7 +(* names for bound variables *)
     1.8 +
     1.9 +local
    1.10 +  fun declare_names (Abs (_, _, b)) = declare_names b
    1.11 +    | declare_names (t $ u) = declare_names t #> declare_names u
    1.12 +    | declare_names (Const (c, _)) = Name.declare (Long_Name.base_name c)
    1.13 +    | declare_names (Free (x, _)) = Name.declare x
    1.14 +    | declare_names _ = I;
    1.15 +
    1.16 +  fun variant_abs bs (Abs (x, T, t)) =
    1.17 +        let
    1.18 +          val names = fold Name.declare bs (declare_names t Name.context);
    1.19 +          val x' = #1 (Name.variant x names);
    1.20 +          val t' = variant_abs (x' :: bs) t;
    1.21 +        in Abs (x', T, t') end
    1.22 +    | variant_abs bs (t $ u) = variant_abs bs t $ variant_abs bs u
    1.23 +    | variant_abs _ t = t;
    1.24 +in
    1.25 +  val named_bounds = variant_abs [];
    1.26 +end;
    1.27 +
    1.28 +
    1.29  (* general setup *)
    1.30  
    1.31  fun setup_presentation f =
    1.32 @@ -89,7 +111,7 @@
    1.33  
    1.34      val encode_const =
    1.35        let open XML.Encode Term_XML.Encode
    1.36 -      in triple (list string) typ (option term) end;
    1.37 +      in triple (list string) typ (option (term o named_bounds)) end;
    1.38  
    1.39      fun export_const c (T, abbrev) =
    1.40        let
    1.41 @@ -113,7 +135,7 @@
    1.42  
    1.43      val encode_props =
    1.44        let open XML.Encode Term_XML.Encode
    1.45 -      in triple (list (pair string sort)) (list (pair string typ)) (list term) end;
    1.46 +      in triple (list (pair string sort)) (list (pair string typ)) (list (term o named_bounds)) end;
    1.47  
    1.48      fun export_props props =
    1.49        let
    1.50 @@ -137,7 +159,7 @@
    1.51  
    1.52      val encode_class =
    1.53        let open XML.Encode Term_XML.Encode
    1.54 -      in pair (list (pair string typ)) (list term) end;
    1.55 +      in pair (list (pair string typ)) (list (term o named_bounds)) end;
    1.56  
    1.57      fun export_class name =
    1.58        (case try (Axclass.get_info thy) name of