# HG changeset patch
# User paulson
# Date 1721675626 -3600
# Node ID 628d2e5015e3ba32bbb96b094d4164d40b45fc64
# Parent  0b8922e351a3eeb7b7ed5ca5d3f1ff324410aa03# Parent  4b5d3d0abb69ff374660a2440a325d5cc9506cfe
merged

diff -r 4b5d3d0abb69 -r 628d2e5015e3 src/Pure/Build/export_theory.ML
--- a/src/Pure/Build/export_theory.ML	Mon Jul 22 20:13:38 2024 +0100
+++ b/src/Pure/Build/export_theory.ML	Mon Jul 22 20:13:46 2024 +0100
@@ -65,17 +65,6 @@
       in ([], triple int string int (ass, delim, pri)) 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);
-
-
 (* locales *)
 
 fun locale_content thy loc =
@@ -149,6 +138,22 @@
     val enabled = export_enabled context;
 
 
+    (* recode *)
+
+    val thy_cache = perhaps ZTerm.init_cache thy;
+
+    val ztyp_of = ZTerm.ztyp_cache thy_cache;
+    val zterm_of = ZTerm.zterm_of thy_cache;
+    val zproof_of = Proofterm.proof_to_zproof thy_cache;
+
+    val encode_ztyp = ZTerm.encode_ztyp;
+    val encode_zterm = ZTerm.encode_zterm {typed_vars = true};
+    val encode_term = encode_zterm o zterm_of;
+
+    val encode_standard_zterm = ZTerm.encode_zterm {typed_vars = false};
+    val encode_standard_zproof = ZTerm.encode_zproof {typed_vars = false};
+
+
     (* strict parents *)
 
     val parents = Theory.parents_of thy;
@@ -228,11 +233,9 @@
 
     (* consts *)
 
-    val encode_term = Term_XML.Encode.term consts;
-
     val encode_const =
       let open XML.Encode Term_XML.Encode
-      in pair encode_syntax (pair (list string) (pair typ (pair (option encode_term) bool))) end;
+      in pair encode_syntax (pair (list string) (pair typ (pair (option encode_zterm) bool))) end;
 
     val _ =
       export_entities "consts" Sign.const_space (#constants (Consts.dest consts))
@@ -242,7 +245,8 @@
               val syntax = get_syntax_const thy_ctxt c;
               val U = Logic.unvarifyT_global T;
               val U0 = Term.strip_sortsT U;
-              val trim_abbrev = Proofterm.standard_vars_term Name.context #> Term.strip_sorts;
+              fun trim_abbrev t =
+                ZTerm.standard_vars Name.context (zterm_of t, NONE) |> #prop |> ZTerm.strip_sorts;
               val abbrev' = Option.map trim_abbrev abbrev;
               val args = map (#1 o dest_TFree) (Consts.typargs consts (c, U0));
               val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0);
@@ -253,19 +257,21 @@
 
     fun standard_prop used extra_shyps raw_prop raw_proof =
       let
-        val (prop, proof) = Proofterm.standard_vars used (raw_prop, raw_proof);
-        val args = rev (add_frees used prop []);
-        val typargs = rev (add_tfrees used prop []);
-        val used_typargs = fold (Name.declare o #1) typargs used;
+        val {typargs, args, prop, proof} =
+          ZTerm.standard_vars used (zterm_of raw_prop, Option.map zproof_of raw_proof);
+        val is_free = not o Name.is_declared used;
+        val args' = args |> filter (is_free o #1);
+        val typargs' = typargs |> filter (is_free o #1);
+        val used_typargs = fold (Name.declare o #1) typargs' used;
         val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps;
-      in ((sorts @ typargs, args, prop), proof) end;
+      in ((sorts @ typargs', args', prop), proof) end;
 
     fun standard_prop_of thm =
       standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm);
 
     val encode_prop =
       let open XML.Encode Term_XML.Encode
-      in triple (list (pair string sort)) (list (pair string typ)) encode_term end;
+      in triple (list (pair string sort)) (list (pair string encode_ztyp)) encode_zterm end;
 
     fun encode_axiom used prop =
       encode_prop (#1 (standard_prop used [] prop NONE));
@@ -308,10 +314,8 @@
         val _ = Thm.expose_proofs thy [thm];
       in
         (prop, deps, proof) |>
-          let
-            open XML.Encode Term_XML.Encode;
-            val encode_proof = Proofterm.encode_standard_proof thy;
-          in triple encode_prop (list Thm_Name.encode) encode_proof end
+          let open XML.Encode Term_XML.Encode
+          in triple encode_prop (list Thm_Name.encode) encode_standard_zproof end
       end;
 
     fun export_thm (thm_id, (thm_name, _)) =
diff -r 4b5d3d0abb69 -r 628d2e5015e3 src/Pure/General/same.ML
--- a/src/Pure/General/same.ML	Mon Jul 22 20:13:38 2024 +0100
+++ b/src/Pure/General/same.ML	Mon Jul 22 20:13:46 2024 +0100
@@ -12,6 +12,7 @@
   type 'a operation = ('a, 'a) function  (*exception SAME*)
   val same: ('a, 'b) function
   val commit: 'a operation -> 'a -> 'a
+  val commit_if: bool -> 'a operation -> 'a -> 'a
   val commit_id: 'a operation -> 'a -> 'a * bool
   val catch: ('a, 'b) function -> 'a -> 'b option
   val compose: 'a operation -> 'a operation -> 'a operation
@@ -31,6 +32,7 @@
 
 fun same _ = raise SAME;
 fun commit f x = f x handle SAME => x;
+fun commit_if b f x = if b then commit f x else f x;
 fun commit_id f x = (f x, false) handle SAME => (x, true);
 
 fun catch f x = SOME (f x) handle SAME => NONE;
diff -r 4b5d3d0abb69 -r 628d2e5015e3 src/Pure/name.ML
--- a/src/Pure/name.ML	Mon Jul 22 20:13:38 2024 +0100
+++ b/src/Pure/name.ML	Mon Jul 22 20:13:46 2024 +0100
@@ -26,11 +26,13 @@
   val build_context: (context -> context) -> context
   val make_context: string list -> context
   val declare: string -> context -> context
+  val declare_renamed: string * string -> context -> context
   val is_declared: context -> string -> bool
   val invent: context -> string -> int -> string list
   val invent_names: context -> string -> 'a list -> (string * 'a) list
   val invent_list: string list -> string -> int -> string list
   val variant: string -> context -> string * context
+  val variant_bound: string -> context -> string * context
   val variant_list: string list -> string list -> string list
   val enforce_case: bool -> string -> string
   val desymbolize: bool option -> string -> string
@@ -101,6 +103,9 @@
 fun declare_renaming (x, x') (Context tab) =
   Context (Symtab.update (clean x, SOME (clean x')) tab);
 
+fun declare_renamed (x, x') =
+  clean x <> clean x' ? declare_renaming (x, x') #> declare x';
+
 fun is_declared (Context tab) = Symtab.defined tab;
 fun declared (Context tab) = Symtab.lookup tab;
 
@@ -144,12 +149,12 @@
         let
           val x0 = Symbol.bump_init x;
           val x' = vary x0;
-          val ctxt' = ctxt
-            |> x0 <> x' ? declare_renaming (x0, x')
-            |> declare x';
+          val ctxt' = ctxt |> declare_renamed (x0, x');
         in (x', ctxt') end;
   in (x' ^ replicate_string n "_", ctxt') end;
 
+fun variant_bound name = variant (if is_bound name then "u" else name);
+
 fun variant_list used names = #1 (make_context used |> fold_map variant names);
 
 
diff -r 4b5d3d0abb69 -r 628d2e5015e3 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Jul 22 20:13:38 2024 +0100
+++ b/src/Pure/proofterm.ML	Mon Jul 22 20:13:46 2024 +0100
@@ -174,11 +174,6 @@
   val expand_name_empty: thm_header -> Thm_Name.P option
   val expand_proof: theory -> (thm_header -> Thm_Name.P option) -> proof -> proof
 
-  val standard_vars: Name.context -> term * proof option -> term * proof option
-  val standard_vars_term: Name.context -> term -> term
-  val add_standard_vars: proof -> (string * typ) list -> (string * typ) list
-  val add_standard_vars_term: term -> (string * typ) list -> (string * typ) list
-
   val export_enabled: unit -> bool
   val export_standard_enabled: unit -> bool
   val export_proof_boxes_required: theory -> bool
@@ -397,7 +392,7 @@
       | zproof (PAxm (a, prop, SOME Ts)) = zproof_const (ZAxiom a) prop Ts
       | zproof (PClass (T, c)) = OFCLASSp (ztyp T, c)
       | zproof (Oracle (a, prop, SOME Ts)) = zproof_const (ZOracle a) prop Ts
-      | zproof (PThm ({serial, command_pos, theory_name, thm_name, prop, types = SOME Ts, ...}, _)) =
+      | zproof (PThm ({serial, theory_name, thm_name, prop, types = SOME Ts, ...}, _)) =
           let val proof_name =
             ZThm {theory_name = theory_name, thm_name = thm_name, serial = serial};
           in zproof_const proof_name prop Ts end;
@@ -2034,110 +2029,6 @@
 
 (** theorems **)
 
-(* standardization of variables for export: only frees and named bounds *)
-
-local
-
-val declare_names_term = Term.declare_term_frees;
-val declare_names_term' = fn SOME t => declare_names_term t | NONE => I;
-val declare_names_proof = fold_proof_terms declare_names_term;
-
-fun variant names bs x =
-  #1 (Name.variant x (fold Name.declare bs names));
-
-fun variant_term bs (Abs (x, T, t)) =
-      let
-        val x' = variant (declare_names_term t Name.context) bs x;
-        val t' = variant_term (x' :: bs) t;
-      in Abs (x', T, t') end
-  | variant_term bs (t $ u) = variant_term bs t $ variant_term bs u
-  | variant_term _ t = t;
-
-fun variant_proof bs (Abst (x, T, prf)) =
-      let
-        val x' = variant (declare_names_proof prf Name.context) bs x;
-        val prf' = variant_proof (x' :: bs) prf;
-      in Abst (x', T, prf') end
-  | variant_proof bs (AbsP (x, t, prf)) =
-      let
-        val x' = variant (declare_names_term' t (declare_names_proof prf Name.context)) bs x;
-        val t' = Option.map (variant_term bs) t;
-        val prf' = variant_proof (x' :: bs) prf;
-      in AbsP (x', t', prf') end
-  | variant_proof bs (prf % t) = variant_proof bs prf % Option.map (variant_term bs) t
-  | variant_proof bs (prf1 %% prf2) = variant_proof bs prf1 %% variant_proof bs prf2
-  | variant_proof bs (Hyp t) = Hyp (variant_term bs t)
-  | variant_proof _ prf = prf;
-
-val used_frees_type = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
-fun used_frees_term t = fold_types used_frees_type t #> Term.declare_term_frees t;
-val used_frees_proof = fold_proof_terms_types used_frees_term used_frees_type;
-
-val unvarifyT = Term.map_atyps (fn TVar ((a, _), S) => TFree (a, S) | T => T);
-val unvarify = Term.map_aterms (fn Var ((x, _), T) => Free (x, T) | t => t) #> map_types unvarifyT;
-val unvarify_proof = map_proof_terms unvarify unvarifyT;
-
-fun hidden_types prop proof =
-  let
-    val visible = (fold_types o fold_atyps) (insert (op =)) prop [];
-    val add_hiddenT = fold_atyps (fn T => not (member (op =) visible T) ? insert (op =) T);
-  in rev (fold_proof_terms_types (fold_types add_hiddenT) add_hiddenT proof []) end;
-
-fun standard_hidden_types term proof =
-  let
-    val hidden = hidden_types term proof;
-    val idx = Term.maxidx_term term (maxidx_proof proof ~1) + 1;
-    fun smash T =
-      if member (op =) hidden T then
-        (case Type.sort_of_atyp T of
-          [] => dummyT
-        | S => TVar (("'", idx), S))
-      else T;
-    val smashT = map_atyps smash;
-  in map_proof_terms (map_types smashT) smashT proof end;
-
-fun standard_hidden_terms term proof =
-  let
-    fun add_unless excluded x =
-      ((is_Free x orelse is_Var x) andalso not (member (op =) excluded x)) ? insert (op =) x;
-    val visible = fold_aterms (add_unless []) term [];
-    val hidden = fold_proof_terms (fold_aterms (add_unless visible)) proof [];
-    val dummy_term = Term.map_aterms (fn x =>
-      if member (op =) hidden x then Term.dummy_pattern (Term.fastype_of x) else x);
-  in proof |> not (null hidden) ? map_proof_terms dummy_term I end;
-
-in
-
-fun standard_vars used (term, opt_proof) =
-  let
-    val proofs = opt_proof
-      |> Option.map (standard_hidden_types term #> standard_hidden_terms term) |> the_list;
-    val proof_terms = rev (fold (fold_proof_terms_types cons (cons o Logic.mk_type)) proofs []);
-    val used_frees = used
-      |> used_frees_term term
-      |> fold used_frees_proof proofs;
-    val inst = Term_Subst.zero_var_indexes_inst used_frees (term :: proof_terms);
-    val term' = term |> Term_Subst.instantiate inst |> unvarify |> variant_term [];
-    val proofs' = proofs |> map (instantiate inst #> unvarify_proof #> variant_proof []);
-  in (term', try hd proofs') end;
-
-fun standard_vars_term used t = #1 (standard_vars used (t, NONE));
-
-val add_standard_vars_term = fold_aterms
-  (fn Free (x, T) =>
-    (fn env =>
-      (case AList.lookup (op =) env x of
-        NONE => (x, T) :: env
-      | SOME T' =>
-          if T = T' then env
-          else raise TYPE ("standard_vars_env: type conflict for variable " ^ quote x, [T, T'], [])))
-    | _ => I);
-
-val add_standard_vars = fold_proof_terms add_standard_vars_term;
-
-end;
-
-
 (* PThm nodes *)
 
 fun prune_body body =
@@ -2168,19 +2059,19 @@
 
 local
 
-fun export_proof thy i prop prf =
+fun export_proof thy i prop0 proof0 =
   let
-    val (prop', SOME prf') = (prop, SOME prf) |> standard_vars Name.context;
-    val args = [] |> add_standard_vars_term prop' |> add_standard_vars prf' |> rev;
-    val typargs = [] |> Term.add_tfrees prop' |> fold_proof_terms Term.add_tfrees prf' |> rev;
-
-    val xml = (typargs, (args, (prop', no_thm_names prf'))) |>
+    val {typargs, args, prop, proof} =
+      ZTerm.standard_vars Name.context
+        (ZTerm.zterm_of thy prop0, SOME (proof_to_zproof thy (no_thm_names proof0)));
+    val xml = (typargs, (args, (prop, the proof))) |>
       let
         open XML.Encode Term_XML.Encode;
-        val encode_vars = list (pair string typ);
-        val encode_term = encode_standard_term thy;
-        val encode_proof = encode_standard_proof thy;
-      in pair (list (pair string sort)) (pair encode_vars (pair encode_term encode_proof)) end;
+        val encode_tfrees = list (pair string sort);
+        val encode_frees = list (pair string ZTerm.encode_ztyp);
+        val encode_term = ZTerm.encode_zterm {typed_vars = false};
+        val encode_proof = ZTerm.encode_zproof {typed_vars = false};
+      in pair encode_tfrees (pair encode_frees (pair encode_term encode_proof)) end;
   in
     Export.export_params (Context.Theory thy)
      {theory_name = Context.theory_long_name thy,
diff -r 4b5d3d0abb69 -r 628d2e5015e3 src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Mon Jul 22 20:13:38 2024 +0100
+++ b/src/Pure/term_subst.ML	Mon Jul 22 20:13:46 2024 +0100
@@ -230,8 +230,10 @@
 (* zero var indexes *)
 
 fun zero_var_inst ins mk (v as ((x, i), X)) (inst, used) =
-  let 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 (ins (v, mk ((x', 0), X)) inst, used') end;
+  let
+    val (x', used') = Name.variant_bound x used;
+    val inst' = if x = x' andalso i = 0 then inst else ins (v, mk ((x', 0), X)) inst;
+  in (inst', used') end;
 
 fun zero_var_indexes_inst used ts =
   let
diff -r 4b5d3d0abb69 -r 628d2e5015e3 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Mon Jul 22 20:13:38 2024 +0100
+++ b/src/Pure/zterm.ML	Mon Jul 22 20:13:46 2024 +0100
@@ -52,6 +52,53 @@
   | fold_types _ _ = I;
 
 
+(* map *)
+
+fun map_tvars_same f =
+  let
+    fun typ (ZTVar v) = f v
+      | typ (ZFun (T, U)) =
+          (ZFun (typ T, Same.commit typ U)
+            handle Same.SAME => ZFun (T, typ U))
+      | typ ZProp = raise Same.SAME
+      | typ (ZType0 _) = raise Same.SAME
+      | typ (ZType1 (a, T)) = ZType1 (a, typ T)
+      | typ (ZType (a, Ts)) = ZType (a, Same.map typ Ts);
+  in typ end;
+
+fun map_aterms_same f =
+  let
+    fun term (ZAbs (x, T, t)) = ZAbs (x, T, term t)
+      | term (ZApp (t, u)) =
+          (ZApp (term t, Same.commit term u)
+            handle Same.SAME => ZApp (t, term u))
+      | term a = f a;
+  in term end;
+
+fun map_vars_same f = map_aterms_same (fn ZVar v => f v | _ => raise Same.SAME);
+
+fun map_types_same f =
+  let
+    fun term (ZVar (xi, T)) = ZVar (xi, f T)
+      | term (ZBound _) = raise Same.SAME
+      | term (ZConst0 _) = raise Same.SAME
+      | term (ZConst1 (c, T)) = ZConst1 (c, f T)
+      | term (ZConst (c, Ts)) = ZConst (c, Same.map f Ts)
+      | term (ZAbs (x, T, t)) =
+          (ZAbs (x, f T, Same.commit term t)
+            handle Same.SAME => ZAbs (x, T, term t))
+      | term (ZApp (t, u)) =
+          (ZApp (term t, Same.commit term u)
+            handle Same.SAME => ZApp (t, term u))
+      | term (OFCLASS (T, c)) = OFCLASS (f T, c);
+  in term end;
+
+val map_tvars = Same.commit o map_tvars_same;
+val map_aterms = Same.commit o map_aterms_same;
+val map_vars = Same.commit o map_vars_same;
+val map_types = Same.commit o map_types_same;
+
+
 (* type ordering *)
 
 local
@@ -224,6 +271,10 @@
   val fold_aterms: (zterm -> 'a -> 'a) -> zterm -> 'a -> 'a
   val fold_vars: (indexname * ztyp -> 'a -> 'a) -> zterm -> 'a -> 'a
   val fold_types: (ztyp -> 'a -> 'a) -> zterm -> 'a -> 'a
+  val map_tvars: (indexname * sort -> ztyp) -> ztyp -> ztyp
+  val map_aterms: (zterm -> zterm) -> zterm -> zterm
+  val map_vars: (indexname * ztyp -> zterm) -> zterm -> zterm
+  val map_types: (ztyp -> ztyp) -> zterm -> zterm
   val ztyp_ord: ztyp ord
   val fast_zterm_ord: zterm ord
   val aconv_zterm: zterm * zterm -> bool
@@ -231,6 +282,8 @@
   val ZAbsps: zterm list -> zproof -> zproof
   val ZAppts: zproof * zterm list -> zproof
   val ZAppps: zproof * zproof list -> zproof
+  val strip_sortsT: ztyp -> ztyp
+  val strip_sorts: zterm -> zterm
   val incr_bv_same: int -> int -> zterm Same.operation
   val incr_proof_bv_same: int -> int -> int -> int -> zproof Same.operation
   val incr_bv: int -> int -> zterm -> zterm
@@ -247,19 +300,28 @@
   val subst_term_same:
     ztyp Same.operation -> (indexname * ztyp, zterm) Same.function -> zterm Same.operation
   exception BAD_INST of ((indexname * ztyp) * zterm) list
+  val fold_proof: {hyps: bool} -> (ztyp -> 'a -> 'a) -> (zterm -> 'a -> 'a) -> zproof -> 'a -> 'a
+  val fold_proof_types: {hyps: bool} -> (ztyp -> 'a -> 'a) -> zproof -> 'a -> 'a
   val map_proof: {hyps: bool} -> ztyp Same.operation -> zterm Same.operation -> zproof -> zproof
   val map_proof_types: {hyps: bool} -> ztyp Same.operation -> zproof -> zproof
   val map_class_proof: (ztyp * class, zproof) Same.function -> zproof -> zproof
+  val maxidx_type: ztyp -> int -> int
+  val maxidx_term: zterm -> int -> int
+  val maxidx_proof: zproof -> int -> int
   val ztyp_of: typ -> ztyp
   val ztyp_dummy: ztyp
   val typ_of_tvar: indexname * sort -> typ
   val typ_of: ztyp -> typ
+  val init_cache: theory -> theory option
+  val exit_cache: theory -> theory option
   val reset_cache: theory -> theory
   val check_cache: theory -> {ztyp: int, typ: int} option
   val ztyp_cache: theory -> typ -> ztyp
   val typ_cache: theory -> ztyp -> typ
   val zterm_cache: theory -> {zterm: term -> zterm, ztyp: typ -> ztyp}
   val zterm_of: theory -> term -> zterm
+  val zterm_dummy_pattern: ztyp -> zterm
+  val zterm_type: ztyp -> zterm
   val term_of: theory -> zterm -> term
   val beta_norm_term_same: zterm Same.operation
   val beta_norm_proof_same: zproof Same.operation
@@ -318,6 +380,8 @@
   val encode_ztyp: ztyp XML.Encode.T
   val encode_zterm: {typed_vars: bool} -> zterm XML.Encode.T
   val encode_zproof: {typed_vars: bool} -> zproof XML.Encode.T
+  val standard_vars: Name.context -> zterm * zproof option ->
+    {typargs: (string * sort) list, args: (string * ztyp) list, prop: zterm, proof: zproof option}
 end;
 
 structure ZTerm: ZTERM =
@@ -345,6 +409,12 @@
 fun combound (t, n, k) =
   if k > 0 then ZApp (combound (t, n + 1, k - 1), ZBound n) else t;
 
+val strip_sortsT_same = map_tvars_same (fn (_, []) => raise Same.SAME | (a, _) => ZTVar (a, []));
+val strip_sorts_same = map_types_same strip_sortsT_same;
+
+val strip_sortsT = Same.commit strip_sortsT_same;
+val strip_sorts = Same.commit strip_sorts_same;
+
 
 (* increment bound variables *)
 
@@ -585,6 +655,17 @@
   in Same.commit proof end;
 
 
+(* maximum index of variables *)
+
+val maxidx_type = fold_tvars (fn ((_, i), _) => Integer.max i);
+
+fun maxidx_term t =
+  fold_types maxidx_type t #>
+  fold_aterms (fn ZVar ((_, i), _) => Integer.max i | _ => I) t;
+
+val maxidx_proof = fold_proof {hyps = false} maxidx_type maxidx_term;
+
+
 (* convert ztyp vs. regular typ *)
 
 fun ztyp_of (TFree (a, S)) = ZTVar ((a, ~1), S)
@@ -622,6 +703,8 @@
 fun make_ztyp_cache () = Typtab.unsynchronized_cache ztyp_of;
 fun make_typ_cache () = ZTypes.unsynchronized_cache typ_of;
 
+in
+
 fun init_cache thy =
   if is_some (Data.get thy) then NONE
   else SOME (Data.put (SOME (make_ztyp_cache (), make_typ_cache ())) thy);
@@ -631,8 +714,6 @@
     SOME (cache1, cache2) => (#reset cache1 (); #reset cache2 (); SOME (Data.put NONE thy))
   | NONE => NONE);
 
-in
-
 val _ = Theory.setup (Theory.at_begin init_cache #> Theory.at_end exit_cache);
 
 fun reset_cache thy =
@@ -682,6 +763,9 @@
 
 val zterm_of = #zterm o zterm_cache;
 
+fun zterm_dummy_pattern T = ZConst1 ("Pure.dummy_pattern", T);
+fun zterm_type T = ZConst1 ("Pure.type", T);
+
 fun term_of thy =
   let
     val instance = Consts.instance (Sign.consts_of thy);
@@ -1427,4 +1511,143 @@
 
 end;
 
+
+(* standardization of variables for export: only frees and named bounds *)
+
+local
+
+fun declare_frees_term t = fold_vars (fn ((x, ~1), _) => Name.declare x | _ => I) t;
+val declare_frees_proof = fold_proof {hyps = true} (K I) declare_frees_term;
+
+val (variant_abs_term, variant_abs_proof) =
+  let
+    fun term bs (ZAbs (x, T, t)) =
+          let
+            val x' = #1 (Name.variant x (declare_frees_term t bs));
+            val bs' = Name.declare x' bs;
+          in ZAbs (x', T, Same.commit_if (x <> x') (term bs') t) end
+      | term bs (ZApp (t, u)) =
+          (ZApp (term bs t, Same.commit (term bs) u)
+            handle Same.SAME => ZApp (t, term bs u))
+      | term _ _ = raise Same.SAME;
+
+    fun proof bs (ZAbst (x, T, p)) =
+          let
+            val x' = #1 (Name.variant x (declare_frees_proof p bs));
+            val bs' = Name.declare x' bs;
+          in ZAbst (x', T, Same.commit_if (x <> x') (proof bs') p) end
+      | proof bs (ZAbsp (x, t, p)) =
+          let
+            val x' = #1 (Name.variant x (declare_frees_term t (declare_frees_proof p bs)));
+            val (t', term_eq) = Same.commit_id (term bs) t;
+            val bs' = Name.declare x' bs;
+          in ZAbsp (x', t', Same.commit_if (x <> x' orelse not term_eq) (proof bs') p) end
+      | proof bs (ZAppt (p, t)) =
+          (ZAppt (proof bs p, Same.commit (term bs) t)
+            handle Same.SAME => ZAppt (p, term bs t))
+      | proof bs (ZAppp (p, q)) =
+          (ZAppp (proof bs p, Same.commit (proof bs) q)
+            handle Same.SAME => ZAppp (p, proof bs q))
+      | proof bs (ZHyp t) = ZHyp (term bs t)
+      | proof _ _ = raise Same.SAME;
+  in (term Name.context, proof Name.context) end;
+
+val used_frees_type = fold_tvars (fn ((a, ~1), _) => Name.declare a | _ => I);
+fun used_frees_term t = fold_types used_frees_type t #> declare_frees_term t;
+val used_frees_proof = fold_proof {hyps = true} used_frees_type used_frees_term;
+
+fun hidden_types prop proof =
+  let
+    val visible = (fold_types o fold_tvars) (insert (op =)) prop [];
+    val add_hiddenT = fold_tvars (fn v => not (member (op =) visible v) ? insert (op =) v);
+  in rev (fold_proof {hyps = true} add_hiddenT (fold_types add_hiddenT) proof []) end;
+
+fun standard_hidden_types prop proof =
+  let
+    val hidden = hidden_types prop proof;
+    val idx = maxidx_term prop (maxidx_proof proof ~1) + 1;
+    fun zvar (v as (_, S)) =
+      if not (member (op =) hidden v) then raise Same.SAME
+      else if null S then ztyp_dummy
+      else ZTVar (("'", idx), S);
+    val typ = map_tvars_same zvar;
+  in proof |> not (null hidden) ? map_proof {hyps = true} typ (map_types typ) end;
+
+fun standard_hidden_terms prop proof =
+  let
+    fun add_unless excluded (ZVar v) = not (member (op =) excluded v) ? insert (op =) v
+      | add_unless _ _ = I;
+    val visible = fold_aterms (add_unless []) prop [];
+    val hidden = fold_proof {hyps = true} (K I) (fold_aterms (add_unless visible)) proof [];
+    fun var (v as (_, T)) =
+      if member (op =) hidden v then zterm_dummy_pattern T else raise Same.SAME;
+    val term = map_vars_same var;
+  in proof |> not (null hidden) ? map_proof {hyps = true} Same.same term end;
+
+fun standard_inst add mk (v as ((x, i), T)) (inst, used) =
+  let
+    val (x', used') = Name.variant_bound x used;
+    val inst' = if x = x' andalso i = ~1 then inst else add (v, mk ((x', ~1), T)) inst;
+  in (inst', used') end;
+
+fun standard_inst_type used prf =
+  let
+    val add_tvars = fold_tvars (fn v => ZTVars.add (v, ()));
+    val (instT, _) =
+      (ZTVars.empty, used) |> ZTVars.fold (standard_inst ZTVars.add ZTVar o #1)
+        (TVars.build (prf |> fold_proof {hyps = true} add_tvars (fold_types add_tvars)));
+  in instantiate_type_same instT end;
+
+fun standard_inst_term used inst_type prf =
+  let
+    val add_vars = fold_vars (fn (x, T) => ZVars.add ((x, Same.commit inst_type T), ()));
+    val (inst, _) =
+      (ZVars.empty, used) |> ZVars.fold (standard_inst ZVars.add ZVar o #1)
+        (ZVars.build (prf |> fold_proof {hyps = true} (K I) add_vars));
+  in instantiate_term_same inst_type inst end;
+
+val typargs_type = fold_tvars (fn ((a, ~1), S) => TFrees.add_set (a, S) | _ => I);
+val typargs_term = fold_types typargs_type;
+val typargs_proof = fold_proof {hyps = true} typargs_type typargs_term;
+
+val add_standard_vars_term = fold_aterms
+  (fn ZVar ((x, ~1), T) =>
+      (fn env =>
+        (case AList.lookup (op =) env x of
+          NONE => (x, T) :: env
+        | SOME T' =>
+            if T = T' then env
+            else
+              raise TYPE ("standard_vars_env: type conflict for variable " ^ quote x,
+                [typ_of T, typ_of T'], [])))
+    | _ => I);
+
+val add_standard_vars = fold_proof {hyps = true} (K I) add_standard_vars_term;
+
+in
+
+fun standard_vars used (prop, opt_prf) =
+  let
+    val prf = the_default ZNop opt_prf
+      |> standard_hidden_types prop
+      |> standard_hidden_terms prop;
+    val prop_prf = ZAppp (ZHyp prop, prf);
+
+    val used' = used |> used_frees_proof prop_prf;
+    val inst_type = standard_inst_type used' prop_prf;
+    val inst_term = standard_inst_term used' inst_type prop_prf;
+    val inst_proof = map_proof_same {hyps = true} inst_type inst_term;
+
+    val prop' = prop |> Same.commit (Same.compose variant_abs_term inst_term);
+    val opt_proof' =
+      if is_none opt_prf then NONE
+      else SOME (prf |> Same.commit (Same.compose variant_abs_proof inst_proof));
+    val proofs' = the_list opt_proof';
+
+    val args = build_rev (add_standard_vars_term prop' #> fold add_standard_vars proofs');
+    val typargs = TFrees.list_set (TFrees.build (typargs_term prop' #> fold typargs_proof proofs'));
+  in {typargs = typargs, args = args, prop = prop', proof = opt_proof'} end;
+
 end;
+
+end;
diff -r 4b5d3d0abb69 -r 628d2e5015e3 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Mon Jul 22 20:13:38 2024 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Mon Jul 22 20:13:46 2024 +0100
@@ -2175,7 +2175,7 @@
   Name,
   uu, uu_, aT,
   clean_index, clean, internal, skolem, is_internal, is_skolem, dest_internal, dest_skolem,
-  Context, declare, declare_renaming, is_declared, declared, context, make_context,
+  Context, declare, declare_renamed, is_declared, declared, context, make_context,
   variant, variant_list
 )
 where
@@ -2242,6 +2242,10 @@
 declare_renaming (x, x') (Context names) =
   Context (Map.insert (clean x) (Just (clean x')) names)
 
+declare_renamed :: (Name, Name) -> Context -> Context
+declare_renamed (x, x') =
+  (if clean x /= clean x' then declare_renaming (x, x') else id) #> declare x'
+
 is_declared :: Context -> Name -> Bool
 is_declared (Context names) x = Map.member x names
 
@@ -2289,9 +2293,7 @@
         let
           x0 = bump_init x
           x' = vary x0
-          ctxt' = ctxt
-            |> (if x0 /= x' then declare_renaming (x0, x') else id)
-            |> declare x'
+          ctxt' = ctxt |> declare_renamed (x0, x')
         in (x', ctxt')
   in (x' <> Bytes.pack (replicate n underscore), ctxt')