--- 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)
})