src/Pure/Thy/export_theory.scala

   case class Prefix(delim: String) extends Syntax
   case class Infix(assoc: Assoc.Value, delim: String, pri: Int) extends Syntax
 
   def decode_syntax: XML.Decode.T[Syntax] =
     XML.Decode.variant(List(
-      { case (Nil, Nil) => No_Syntax },
-      { case (List(delim), Nil) => Prefix(delim) },
+      { case (Nil, Nil) => No_Syntax case _ => ??? },
+      { case (List(delim), Nil) => Prefix(delim) case _ => ??? },
       { case (Nil, body) =>
           import XML.Decode._
           val (ass, delim, pri) = triple(int, string, int)(body)
-          Infix(Assoc(ass), delim, pri) }))
+          Infix(Assoc(ass), delim, pri)
+        case _ => ??? }))
 
 
   /* types */
 
   sealed case class Type(syntax: Syntax, args: List[String], abbrev: Option[Term.Typ])

   case object Unknown_Recursion extends Recursion
 
   val decode_recursion: XML.Decode.T[Recursion] = {
     import XML.Decode._
     variant(List(
-      { case (Nil, a) => Primrec(list(string)(a)) },
-      { case (Nil, Nil) => Recdef },
-      { case (Nil, a) => Primcorec(list(string)(a)) },
-      { case (Nil, Nil) => Corec },
-      { case (Nil, Nil) => Unknown_Recursion }))
+      { case (Nil, a) => Primrec(list(string)(a)) case _ => ??? },
+      { case (Nil, Nil) => Recdef case _ => ??? },
+      { case (Nil, a) => Primcorec(list(string)(a)) case _ => ??? },
+      { case (Nil, Nil) => Corec case _ => ??? },
+      { case (Nil, Nil) => Unknown_Recursion case _ => ??? }))
   }
 
 
   sealed abstract class Rough_Classification {
     def is_equational: Boolean = this.isInstanceOf[Equational]

   case object Unknown extends Rough_Classification
 
   val decode_rough_classification: XML.Decode.T[Rough_Classification] = {
     import XML.Decode._
     variant(List(
-      { case (Nil, a) => Equational(decode_recursion(a)) },
-      { case (Nil, Nil) => Inductive },
-      { case (Nil, Nil) => Co_Inductive },
-      { case (Nil, Nil) => Unknown }))
+      { case (Nil, a) => Equational(decode_recursion(a)) case _ => ??? },
+      { case (Nil, Nil) => Inductive case _ => ??? },
+      { case (Nil, Nil) => Co_Inductive case _ => ??? },
+      { case (Nil, Nil) => Unknown case _ => ??? }))
   }
 
 
   sealed case class Spec_Rule(
     pos: Position.T,