src/Pure/Thy/export_theory.scala

--- a/src/Pure/Thy/export_theory.scala	Thu Sep 27 07:18:34 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Fri Sep 28 19:30:07 2018 +0200
@@ -362,13 +362,13 @@
   sealed case class Locale(
     entity: Entity,
     typargs: List[(String, Term.Sort)],
-    args: List[(String, Term.Typ)],
+    args: List[((String, Term.Typ), Option[Infix])],
     axioms: List[Prop])
   {
     def cache(cache: Term.Cache): Locale =
       Locale(entity.cache(cache),
         typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
-        args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
+        args.map({ case ((name, typ), syntax) => ((cache.string(name), cache.typ(typ)), syntax) }),
         axioms.map(_.cache(cache)))
   }
 
@@ -380,7 +380,8 @@
         {
           import XML.Decode._
           import Term_XML.Decode._
-          triple(list(pair(string, sort)), list(pair(string, typ)), list(decode_prop))(body)
+          triple(list(pair(string, sort)), list(pair(pair(string, typ), option(decode_infix))),
+            list(decode_prop))(body)
         }
         Locale(entity, typargs, args, axioms)
       })