# HG changeset patch
# User wenzelm
# Date 1649498871 -7200
# Node ID 323481d143c6ec49a153646133ffb73136f00965
# Parent  7ae5df33ff230f007083e8e0b0cbdb01d2958e28
tuned --- avoid warnings in scala3;

diff -r 7ae5df33ff23 -r 323481d143c6 src/Pure/term_xml.scala
--- a/src/Pure/term_xml.scala	Sat Apr 09 12:03:56 2022 +0200
+++ b/src/Pure/term_xml.scala	Sat Apr 09 12:07:51 2022 +0200
@@ -50,7 +50,7 @@
       variant[Typ](List(
         { case (List(a), b) => Type(a, list(typ)(b)) case _ => ??? },
         { case (List(a), b) => TFree(a, sort(b)) case _ => ??? },
-        { case (a, b) => TVar(indexname(a), sort(b)) case _ => ??? }))
+        { case (a, b) => TVar(indexname(a), sort(b)) }))
 
     val typ_body: T[Typ] = { case Nil => dummyT case body => typ(body) }
 
@@ -58,7 +58,7 @@
       variant[Term](List(
         { case (List(a), b) => Const(a, list(typ)(b)) case _ => ??? },
         { case (List(a), b) => Free(a, typ_body(b)) case _ => ??? },
-        { case (a, b) => Var(indexname(a), typ_body(b)) case _ => ??? },
+        { case (a, b) => Var(indexname(a), typ_body(b)) },
         { case (Nil, a) => Bound(int(a)) case _ => ??? },
         { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) case _ => ??? },
         { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) case _ => ??? }))
@@ -71,7 +71,7 @@
         variant[Term](List(
           { case (List(a), b) => Const(a, list(typ)(b)) case _ => ??? },
           { case (List(a), b) => Free(a, env_type(a, typ_body(b))) case _ => ??? },
-          { case (a, b) => Var(indexname(a), typ_body(b)) case _ => ??? },
+          { case (a, b) => Var(indexname(a), typ_body(b)) },
           { case (Nil, a) => Bound(int(a)) case _ => ??? },
           { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) case _ => ??? },
           { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) case _ => ??? }))