# HG changeset patch
# User wenzelm
# Date 1535725050 -7200
# Node ID 1dacce27bc25be3a1ca3954ff4235d9fb7270c79
# Parent  a0769c7f51b4e3206c5a5b19b967287c3a7d9634
clarified signature: proper typargs;

diff -r a0769c7f51b4 -r 1dacce27bc25 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Fri Aug 31 15:57:21 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Fri Aug 31 16:17:30 2018 +0200
@@ -198,13 +198,17 @@
 
     (* locales *)
 
-    fun encode_locale {type_params, params, asm, defs} =
-      (type_params, (map #1 params, (asm, defs))) |>
-        let open XML.Encode Term_XML.Encode in
-          pair (list (pair string sort))
-            (pair (list (pair string typ))
-              (pair (option term) (list term)))
-        end;
+    fun encode_locale ({type_params, params, asm, defs}: Locale.content) =
+      let
+        val args = map #1 params;
+        val typargs = type_params @ rev (fold Term.add_tfrees (map Free args @ the_list asm) []);
+        val encode =
+          let open XML.Encode Term_XML.Encode in
+            pair (list (pair string sort))
+              (pair (list (pair string typ))
+                (pair (option term) (list term)))
+          end;
+      in encode (typargs, (args, (asm, defs))) end;
 
     val _ =
       export_entities "locales" (fn _ => SOME o encode_locale) Locale.locale_space
diff -r a0769c7f51b4 -r 1dacce27bc25 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Fri Aug 31 15:57:21 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Fri Aug 31 16:17:30 2018 +0200
@@ -327,13 +327,13 @@
   /* locales */
 
   sealed case class Locale(
-    entity: Entity, type_params: List[(String, Term.Sort)], params: List[(String, Term.Typ)],
+    entity: Entity, typargs: List[(String, Term.Sort)], args: List[(String, Term.Typ)],
       asm: Option[Term.Term], defs: List[Term.Term])
   {
     def cache(cache: Term.Cache): Locale =
       Locale(entity.cache(cache),
-        type_params.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
-        params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
+        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
+        args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
         asm.map(cache.term(_)),
         defs.map(cache.term(_)))
   }
@@ -342,7 +342,7 @@
     provider.uncompressed_yxml(export_prefix + "locales").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.LOCALE, tree)
-        val (type_params, (params, (asm, defs))) =
+        val (typargs, (args, (asm, defs))) =
         {
           import XML.Decode._
           import Term_XML.Decode._
@@ -350,7 +350,7 @@
             pair(list(pair(string, typ)),
               pair(option(term), list(term))))(body)
         }
-        Locale(entity, type_params, params, asm, defs)
+        Locale(entity, typargs, args, asm, defs)
       })