# HG changeset patch
# User wenzelm
# Date 1565803294 -7200
# Node ID 2ecbbe6b35db531f74d9b28c580d565467b76213
# Parent  9b3610fe74d62d9444fd14323219e6b866aba15e
uniform standard_vars for terms and proof terms;

diff -r 9b3610fe74d6 -r 2ecbbe6b35db 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;
diff -r 9b3610fe74d6 -r 2ecbbe6b35db src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Aug 14 11:14:27 2019 +0200
+++ b/src/Pure/proofterm.ML	Wed Aug 14 19:21:34 2019 +0200
@@ -162,6 +162,10 @@
   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_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
   val thm_proof: theory -> (class * class -> proof) ->
@@ -1979,6 +1983,82 @@
 
 (** theorems **)
 
+(* standardization of variables for export: only frees and named bounds *)
+
+local
+
+fun declare_names_term (Abs (_, _, b)) = declare_names_term b
+  | declare_names_term (t $ u) = declare_names_term t #> declare_names_term u
+  | declare_names_term (Const (c, _)) = Name.declare (Long_Name.base_name c)
+  | declare_names_term (Free (x, _)) = Name.declare x
+  | declare_names_term _ = I;
+
+val declare_names_term' = fn SOME t => declare_names_term t | NONE => I;
+
+fun declare_names_proof (Abst (_, _, prf)) = declare_names_proof prf
+  | declare_names_proof (AbsP (_, t, prf)) = declare_names_term' t #> declare_names_proof prf
+  | declare_names_proof (prf % t) = declare_names_proof prf #> declare_names_term' t
+  | declare_names_proof (prf1 %% prf2) = declare_names_proof prf1 #> declare_names_proof prf2
+  | declare_names_proof _ = I;
+
+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;
+
+in
+
+fun standard_vars used (terms, proofs) =
+  let
+    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 is_used = Name.is_declared used o Name.clean;
+    fun unvarifyT ty = ty |> Term.map_atyps
+      (fn TVar ((a, _), S) => TFree (a, S)
+        | T as TFree (a, _) => if is_used a then T else raise TYPE (Logic.bad_fixed a, [ty], [])
+        | T => T);
+    fun unvarify tm = tm |> Term.map_aterms
+      (fn Var ((x, _), T) => Free (x, T)
+        | t as Free (x, _) => if is_used x then t else raise TERM (Logic.bad_fixed x, [tm])
+        | t => t);
+
+    val terms' = terms
+      |> map (Term_Subst.instantiate inst #> unvarify #> map_types unvarifyT #> 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;
+
+end;
+
+
+(* PThm nodes *)
+
 val proof_serial = Counter.make ();
 
 local
@@ -2021,9 +2101,18 @@
 
 end;
 
+val declare_freesT = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
+fun declare_frees t =
+  fold_types declare_freesT t #>
+  fold_aterms (fn Free (x, _) => Name.declare x | _ => I) t;
+
 fun export_proof thy i prop prf =
   let
-    val xml = reconstruct_proof thy prop prf |> encode_export prop;
+    val free_names = Name.context
+      |> declare_frees prop
+      |> fold_proof_terms declare_frees declare_freesT prf;
+    val ([prop'], [prf']) = standard_vars free_names ([prop], [reconstruct_proof thy prop prf]);
+    val xml = encode_export prop' prf';
     val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty);
   in
     chunks |> Export.export_params