# HG changeset patch
# User wenzelm
# Date 1587570734 -7200
# Node ID 3fd54f7f52b0dac12c8f1817a31883a07f7b4569
# Parent  21adf2ed442c6d302f6942c1bc5bc15bb9259b2a
tuned signature -- avoid warnings;

diff -r 21adf2ed442c -r 3fd54f7f52b0 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Wed Apr 22 13:45:02 2020 +0200
+++ b/src/Pure/General/pretty.scala	Wed Apr 22 17:52:14 2020 +0200
@@ -76,7 +76,7 @@
       val (line, rest) =
         Library.take_prefix[Tree]({ case Break(true, _, _) => false case _ => true }, prts)
       val len1 = ((0.0 /: line) { case (l, t) => l + t.length }) max len
-      rest match {
+      (rest: @unchecked) match {
         case Break(true, _, ind) :: rest1 =>
           body_length(Break(false, indent1 + ind, 0) :: rest1, len1)
         case Nil => len1
diff -r 21adf2ed442c -r 3fd54f7f52b0 src/Pure/term.scala
--- a/src/Pure/term.scala	Wed Apr 22 13:45:02 2020 +0200
+++ b/src/Pure/term.scala	Wed Apr 22 17:52:14 2020 +0200
@@ -195,7 +195,7 @@
         lookup(x) match {
           case Some(y) => y
           case None =>
-            x match {
+            (x: @unchecked) match {
               case PBound(_) => store(x)
               case Abst(name, typ, body) =>
                 store(Abst(cache_string(name), cache_typ(typ), cache_proof(body)))