# HG changeset patch
# User wenzelm
# Date 1575297017 -3600
# Node ID 37eb175895c50a3913c38812b018a69d50e18f90
# Parent  5727bcc3c47c826296a077f748d995f843fcb5bb
proper treatment of variable names;

diff -r 5727bcc3c47c -r 37eb175895c5 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Mon Dec 02 15:04:38 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Mon Dec 02 15:30:17 2019 +0100
@@ -122,19 +122,20 @@
 
 (* spec rules *)
 
-fun spec_rule_content {pos, name, rough_classification, terms = terms0, rules = rules0} =
+fun spec_rule_content {pos, name, rough_classification, terms, rules} =
   let
-    val terms = map Logic.unvarify_global terms0;
-    val rules = map (Logic.unvarify_global o Thm.plain_prop_of) rules0;
-    val text = terms @ rules;
+    val spec =
+      terms @ map Thm.plain_prop_of rules
+      |> Term_Subst.zero_var_indexes_list
+      |> map Logic.unvarify_global;
   in
    {props = Position.properties_of pos,
     name = name,
     rough_classification = rough_classification,
-    typargs = rev (fold Term.add_tfrees text []),
-    args = rev (fold Term.add_frees text []),
-    terms = map (fn t => (t, Term.type_of t)) terms,
-    rules = rules}
+    typargs = rev (fold Term.add_tfrees spec []),
+    args = rev (fold Term.add_frees spec []),
+    terms = map (fn t => (t, Term.type_of t)) (take (length terms) spec),
+    rules = drop (length terms) spec}
   end;