src/Pure/Thy/export_theory.scala
changeset 68173 7ed88a534bb6
parent 68172 0f14cf9c632f
child 68203 cda4f24331d5
     1.1 --- a/src/Pure/Thy/export_theory.scala	Sun May 13 20:24:33 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.scala	Sun May 13 21:20:28 2018 +0200
     1.3 @@ -34,9 +34,6 @@
     1.4    /* types */
     1.5  
     1.6    sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
     1.7 -  {
     1.8 -    def arity: Int = args.length
     1.9 -  }
    1.10  
    1.11    def decode_type(tree: XML.Tree): Type =
    1.12    {
    1.13 @@ -52,16 +49,17 @@
    1.14  
    1.15    /* consts */
    1.16  
    1.17 -  sealed case class Const(entity: Entity, typ: Term.Typ, abbrev: Option[Term.Term])
    1.18 +  sealed case class Const(
    1.19 +    entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
    1.20  
    1.21    def decode_const(tree: XML.Tree): Const =
    1.22    {
    1.23      val (entity, body) = decode_entity(tree)
    1.24 -    val (typ, abbrev) =
    1.25 +    val (args, typ, abbrev) =
    1.26      {
    1.27        import XML.Decode._
    1.28 -      pair(Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
    1.29 +      triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
    1.30      }
    1.31 -    Const(entity, typ, abbrev)
    1.32 +    Const(entity, args, typ, abbrev)
    1.33    }
    1.34  }