diff -r 2d5c313e8582 -r 8f2d3a27aff0 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Wed Mar 27 12:08:08 2019 +0100
+++ b/src/Pure/Thy/export_theory.scala	Wed Mar 27 14:47:49 2019 +0100
@@ -253,7 +253,8 @@
     typ: Term.Typ,
     abbrev: Option[Term.Term],
     propositional: Boolean,
-    primrec_types: List[String])
+    primrec_types: List[String],
+    corecursive: Boolean)
   {
     def cache(cache: Term.Cache): Const =
       Const(entity.cache(cache),
@@ -262,22 +263,24 @@
         cache.typ(typ),
         abbrev.map(cache.term(_)),
         propositional,
-        primrec_types.map(cache.string(_)))
+        primrec_types.map(cache.string(_)),
+        corecursive)
   }
 
   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))))) =
+        val (syntax, (args, (typ, (abbrev, (propositional, (primrec_types, corecursive)))))) =
         {
           import XML.Decode._
           pair(decode_syntax,
             pair(list(string),
               pair(Term_XML.Decode.typ,
-                pair(option(Term_XML.Decode.term), pair(bool, list(string))))))(body)
+                pair(option(Term_XML.Decode.term), pair(bool,
+                  pair(list(string), bool))))))(body)
         }
-        Const(entity, syntax, args, typ, abbrev, propositional, primrec_types)
+        Const(entity, syntax, args, typ, abbrev, propositional, primrec_types, corecursive)
       })