--- a/src/Pure/Thy/export_theory.scala Tue Dec 03 15:59:01 2019 +0100
+++ b/src/Pure/Thy/export_theory.scala Tue Dec 03 16:40:04 2019 +0100
@@ -284,9 +284,7 @@
typargs: List[String],
typ: Term.Typ,
abbrev: Option[Term.Term],
- propositional: Boolean,
- primrec_types: List[String],
- corecursive: Boolean)
+ propositional: Boolean)
{
def cache(cache: Term.Cache): Const =
Const(entity.cache(cache),
@@ -294,25 +292,22 @@
typargs.map(cache.string(_)),
cache.typ(typ),
abbrev.map(cache.term(_)),
- propositional,
- primrec_types.map(cache.string(_)),
- corecursive)
+ propositional)
}
def read_consts(provider: Export.Provider): List[Const] =
provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
{
val (entity, body) = decode_entity(Kind.CONST, tree)
- val (syntax, (args, (typ, (abbrev, (propositional, (primrec_types, corecursive)))))) =
+ val (syntax, (typargs, (typ, (abbrev, propositional)))) =
{
import XML.Decode._
pair(decode_syntax,
pair(list(string),
pair(Term_XML.Decode.typ,
- pair(option(Term_XML.Decode.term), pair(bool,
- pair(list(string), bool))))))(body)
+ pair(option(Term_XML.Decode.term), bool))))(body)
}
- Const(entity, syntax, args, typ, abbrev, propositional, primrec_types, corecursive)
+ Const(entity, syntax, typargs, typ, abbrev, propositional)
})