src/Pure/Thy/export_theory.scala
changeset 68864 1dacce27bc25
parent 68862 47e9912c53c3
child 68997 4278947ba336
     1.1 --- a/src/Pure/Thy/export_theory.scala	Fri Aug 31 15:57:21 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.scala	Fri Aug 31 16:17:30 2018 +0200
     1.3 @@ -327,13 +327,13 @@
     1.4    /* locales */
     1.5  
     1.6    sealed case class Locale(
     1.7 -    entity: Entity, type_params: List[(String, Term.Sort)], params: List[(String, Term.Typ)],
     1.8 +    entity: Entity, typargs: List[(String, Term.Sort)], args: List[(String, Term.Typ)],
     1.9        asm: Option[Term.Term], defs: List[Term.Term])
    1.10    {
    1.11      def cache(cache: Term.Cache): Locale =
    1.12        Locale(entity.cache(cache),
    1.13 -        type_params.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
    1.14 -        params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
    1.15 +        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
    1.16 +        args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
    1.17          asm.map(cache.term(_)),
    1.18          defs.map(cache.term(_)))
    1.19    }
    1.20 @@ -342,7 +342,7 @@
    1.21      provider.uncompressed_yxml(export_prefix + "locales").map((tree: XML.Tree) =>
    1.22        {
    1.23          val (entity, body) = decode_entity(Kind.LOCALE, tree)
    1.24 -        val (type_params, (params, (asm, defs))) =
    1.25 +        val (typargs, (args, (asm, defs))) =
    1.26          {
    1.27            import XML.Decode._
    1.28            import Term_XML.Decode._
    1.29 @@ -350,7 +350,7 @@
    1.30              pair(list(pair(string, typ)),
    1.31                pair(option(term), list(term))))(body)
    1.32          }
    1.33 -        Locale(entity, type_params, params, asm, defs)
    1.34 +        Locale(entity, typargs, args, asm, defs)
    1.35        })
    1.36  
    1.37