src/Pure/term_xml.scala
changeset 75393 87ebf5a50283
parent 71777 3875815f5967
child 75425 b958e053d993
--- a/src/Pure/term_xml.scala	Fri Apr 01 11:51:42 2022 +0200
+++ b/src/Pure/term_xml.scala	Fri Apr 01 17:06:10 2022 +0200
@@ -7,12 +7,10 @@
 package isabelle
 
 
-object Term_XML
-{
+object Term_XML {
   import Term._
 
-  object Encode
-  {
+  object Encode {
     import XML.Encode._
 
     val indexname: P[Indexname] =
@@ -39,8 +37,7 @@
         { case App(a, b) => (Nil, pair(term, term)(a, b)) }))
   }
 
-  object Decode
-  {
+  object Decode {
     import XML.Decode._
 
     val indexname: P[Indexname] =
@@ -66,8 +63,7 @@
         { 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
 
@@ -82,8 +78,7 @@
       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(