diff -r 66fa99c85095 -r 7d522732b7f2 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Mon Dec 02 12:03:55 2019 +0100
+++ b/src/Pure/Thy/export_theory.scala	Mon Dec 02 13:03:09 2019 +0100
@@ -716,7 +716,7 @@
     rough_classification: Rough_Classification,
     typargs: List[(String, Term.Sort)],
     args: List[(String, Term.Typ)],
-    terms: List[Term.Term],
+    terms: List[(Term.Term, Term.Typ)],
     rules: List[Term.Term])
   {
     def id: Option[Long] = Position.Id.unapply(pos)
@@ -728,7 +728,7 @@
         rough_classification.cache(cache),
         typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
         args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
-        terms.map(cache.term(_)),
+        terms.map({ case (term, typ) => (cache.term(term), cache.typ(typ)) }),
         rules.map(cache.term(_)))
   }
 
@@ -742,7 +742,7 @@
       list(
         pair(properties, pair(string, pair(decode_rough_classification,
           pair(list(pair(string, sort)), pair(list(pair(string, typ)),
-            pair(list(term), list(term))))))))(body)
+            pair(list(pair(term, typ)), list(term))))))))(body)
     }
     for ((pos, (name, (rough_classification, (typargs, (args, (terms, rules)))))) <- spec_rules)
       yield Spec_Rule(pos, name, rough_classification, typargs, args, terms, rules)