src/Pure/term_xml.scala

 */
 
 package isabelle
 
 
-object Term_XML
-{
+object Term_XML {
   import Term._
 
-  object Encode
-  {
+  object Encode {
     import XML.Encode._
 
     val indexname: P[Indexname] =
       { case Indexname(a, 0) => List(a)
         case Indexname(a, b) => List(a, int_atom(b)) }

         { case Bound(a) => (Nil, int(a)) },
         { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
         { case App(a, b) => (Nil, pair(term, term)(a, b)) }))
   }
 
-  object Decode
-  {
+  object Decode {
     import XML.Decode._
 
     val indexname: P[Indexname] =
       { case List(a) => Indexname(a, 0)
         case List(a, b) => Indexname(a, int_atom(b)) }

         { case (a, b) => Var(indexname(a), typ_body(b)) },
         { case (Nil, a) => Bound(int(a)) },
         { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
         { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
 
-    def term_env(env: Map[String, Typ]): T[Term] =
-    {
+    def term_env(env: Map[String, Typ]): T[Term] = {
       def env_type(x: String, t: Typ): Typ =
         if (t == dummyT && env.isDefinedAt(x)) env(x) else t
 
       def term: T[Term] =
         variant[Term](List(

           { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
           { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
       term
     }
 
-    def proof_env(env: Map[String, Typ]): T[Proof] =
-    {
+    def proof_env(env: Map[String, Typ]): T[Proof] = {
       val term = term_env(env)
       def proof: T[Proof] =
         variant[Proof](List(
           { case (Nil, Nil) => MinProof },
           { case (Nil, a) => PBound(int(a)) },