# HG changeset patch
# User wenzelm
# Date 1565896686 -7200
# Node ID f3fbc7f3559d3d73153d532d30874366ef158c90
# Parent  04ef5ee3dd4ddc353180b48a5ed7a4951c5b9c79
more careful treatment of hidden type variable names: smash before zero_var_indexes to get standard enumeration;

diff -r 04ef5ee3dd4d -r f3fbc7f3559d src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Thu Aug 15 19:35:17 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Thu Aug 15 21:18:06 2019 +0200
@@ -222,14 +222,12 @@
 
     fun standard_prop used extra_shyps raw_prop raw_proof =
       let
-        val raw_proofs = the_list raw_proof;
-        val ([prop], proofs) = Proofterm.standard_vars used ([raw_prop], raw_proofs);
-
+        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 sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps;
-      in ((sorts @ typargs, args, prop), try hd proofs) end;
+      in ((sorts @ typargs, args, prop), proof) end;
 
     val encode_prop =
       let open XML.Encode Term_XML.Encode
diff -r 04ef5ee3dd4d -r f3fbc7f3559d src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Aug 15 19:35:17 2019 +0200
+++ b/src/Pure/proofterm.ML	Thu Aug 15 21:18:06 2019 +0200
@@ -165,9 +165,8 @@
   val prop_of: proof -> term
   val expand_proof: theory -> (string * term option) list -> proof -> proof
 
-  val standard_vars: Name.context -> term list * proof list -> term list * proof list
+  val standard_vars: Name.context -> term * proof option -> term * proof option
   val standard_vars_term: Name.context -> term -> term
-  val standard_vars_proof: Name.context -> proof -> proof
 
   val proof_serial: unit -> proof_serial
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
@@ -2049,25 +2048,37 @@
 
 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 (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 TVar (("'", idx), Type.sort_of_atyp T) else T;
+    val smashT = map_atyps smash;
+  in map_proof_terms (map_types smashT) smashT proof end;
 
 in
 
-fun standard_vars used (terms, proofs) =
+fun standard_vars used (term, opt_proof) =
   let
-    val used' = used
-      |> fold used_frees_term terms
+    val proofs = the_list (Option.map (standard_hidden_types term) opt_proof);
+    val proof_terms = rev (fold (fold_proof_terms cons (cons o Logic.mk_type)) proofs []);
+    val used_frees = used
+      |> used_frees_term term
       |> fold used_frees_proof proofs;
-    val proof_terms = rev ((fold (fold_proof_terms cons (cons o Logic.mk_type))) proofs []);
-    val inst = Term_Subst.zero_var_indexes_inst used' (terms @ proof_terms);
+    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;
 
-    val terms' = terms
-      |> map (Term_Subst.instantiate inst #> unvarify #> variant_term []);
-    val proofs' = proofs
-      |> map (instantiate inst #> map_proof_terms unvarify unvarifyT #> variant_proof []);
-  in (terms', proofs') end;
-
-fun standard_vars_term used t = standard_vars used ([t], []) |> #1 |> the_single;
-fun standard_vars_proof used prf = standard_vars used ([], [prf]) |> #2 |> the_single;
+fun standard_vars_term used t = #1 (standard_vars used (t, NONE));
 
 end;
 
@@ -2102,7 +2113,8 @@
 
 fun export_proof thy i prop prf =
   let
-    val ([prop'], [prf']) = standard_vars Name.context ([prop], [reconstruct_proof thy prop prf]);
+    val (prop', SOME prf') =
+      standard_vars Name.context (prop, SOME (reconstruct_proof thy prop prf));
     val xml = encode_export prop' prf';
     val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty);
   in