diff --git a/src/Pure/General/pretty.scala b/src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala
+++ b/src/Pure/General/pretty.scala
@@ -1,189 +1,189 @@
 /*  Title:      Pure/General/pretty.scala
     Author:     Makarius
 
 Generic pretty printing module.
 */
 
 package isabelle
 
 import scala.annotation.tailrec
 
 
 object Pretty
 {
   /* XML constructors */
 
   val space: XML.Body = List(XML.Text(Symbol.space))
   def spaces(n: Int): XML.Body =
     if (n == 0) Nil
     else if (n == 1) space
     else List(XML.Text(Symbol.spaces(n)))
 
   def block(consistent: Boolean, indent: Int, body: XML.Body): XML.Tree =
     XML.Elem(Markup.Block(consistent, indent), body)
   def block(indent: Int, body: XML.Body): XML.Tree = block(false, indent, body)
   def block(body: XML.Body): XML.Tree = block(2, body)
 
   def brk(width: Int, indent: Int = 0): XML.Tree =
     XML.Elem(Markup.Break(width, indent), spaces(width))
 
   val fbrk: XML.Tree = XML.newline
   def fbreaks(ts: List[XML.Tree]): XML.Body = Library.separate(fbrk, ts)
 
   val Separator: XML.Body = List(XML.elem(Markup.SEPARATOR, space), fbrk)
   def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
 
 
   /* text metric -- standardized to width of space */
 
   abstract class Metric
   {
     val unit: Double
     def apply(s: String): Double
   }
 
   object Default_Metric extends Metric
   {
     val unit = 1.0
     def apply(s: String): Double = s.length.toDouble
   }
 
 
   /* markup trees with physical blocks and breaks */
 
   private def force_nat(i: Int): Int = i max 0
 
   private sealed abstract class Tree { def length: Double }
   private case class Block(
     markup: Option[(Markup, Option[XML.Body])],
     consistent: Boolean, indent: Int, body: List[Tree], length: Double) extends Tree
   private case class Break(force: Boolean, width: Int, indent: Int) extends Tree
   { def length: Double = width.toDouble }
   private case class Str(string: String, length: Double) extends Tree
 
   private val FBreak = Break(true, 1, 0)
 
   private def make_block(
       markup: Option[(Markup, Option[XML.Body])],
       consistent: Boolean,
       indent: Int,
       body: List[Tree]): Tree =
   {
     val indent1 = force_nat(indent)
 
     @tailrec def body_length(prts: List[Tree], len: Double): Double =
     {
       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
       }
     }
     Block(markup, consistent, indent1, body, body_length(body, 0.0))
   }
 
 
   /* formatted output */
 
   private sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0)
   {
     def newline: Text = copy(tx = fbrk :: tx, pos = 0.0, nl = nl + 1)
     def string(s: String, len: Double): Text =
       copy(tx = if (s == "") tx else XML.Text(s) :: tx, pos = pos + len)
     def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
     def content: XML.Body = tx.reverse
   }
 
   private def break_dist(trees: List[Tree], after: Double): Double =
     trees match {
       case (_: Break) :: _ => 0.0
       case t :: ts => t.length + break_dist(ts, after)
       case Nil => after
     }
 
   private def force_break(tree: Tree): Tree =
     tree match { case Break(false, wd, ind) => Break(true, wd, ind) case _ => tree }
   private def force_all(trees: List[Tree]): List[Tree] = trees.map(force_break)
 
   private def force_next(trees: List[Tree]): List[Tree] =
     trees match {
       case Nil => Nil
       case (t: Break) :: ts => force_break(t) :: ts
       case t :: ts => t :: force_next(ts)
     }
 
   val default_margin: Double = 76.0
   val default_breakgain: Double = default_margin / 20
 
   def formatted(input: XML.Body,
     margin: Double = default_margin,
     breakgain: Double = default_breakgain,
     metric: Metric = Default_Metric): XML.Body =
   {
     val emergencypos = (margin / 2).round.toInt
 
     def make_tree(inp: XML.Body): List[Tree] =
       inp flatMap {
         case XML.Wrapped_Elem(markup, body1, body2) =>
           List(make_block(Some(markup, Some(body1)), false, 0, make_tree(body2)))
         case XML.Elem(markup, body) =>
           markup match {
             case Markup.Block(consistent, indent) =>
               List(make_block(None, consistent, indent, make_tree(body)))
             case Markup.Break(width, indent) =>
               List(Break(false, force_nat(width), force_nat(indent)))
             case Markup(Markup.ITEM, _) =>
               List(make_block(None, false, 2,
                 make_tree(XML.elem(Markup.BULLET, space) :: space ::: body)))
             case _ =>
               List(make_block(Some((markup, None)), false, 0, make_tree(body)))
           }
         case XML.Text(text) =>
           Library.separate(FBreak, split_lines(text).map(s => Str(s, metric(s))))
       }
 
     def format(trees: List[Tree], blockin: Int, after: Double, text: Text): Text =
       trees match {
         case Nil => text
 
         case Block(markup, consistent, indent, body, blen) :: ts =>
           val pos1 = (text.pos + indent).ceil.toInt
           val pos2 = pos1 % emergencypos
           val blockin1 = if (pos1 < emergencypos) pos1 else pos2
           val d = break_dist(ts, after)
           val body1 = if (consistent && text.pos + blen > margin - d) force_all(body) else body
           val btext =
             markup match {
               case None => format(body1, blockin1, d, text)
               case Some((m, markup_body)) =>
                 val btext0 = format(body1, blockin1, d, text.copy(tx = Nil))
                 val elem =
                   markup_body match {
                     case None => XML.Elem(m, btext0.content)
                     case Some(b) => XML.Wrapped_Elem(m, b, btext0.content)
                   }
                 btext0.copy(tx = elem :: text.tx)
             }
           val ts1 = if (text.nl < btext.nl) force_next(ts) else ts
           format(ts1, blockin, after, btext)
 
         case Break(force, wd, ind) :: ts =>
           if (!force &&
               text.pos + wd <= ((margin - break_dist(ts, after)) max (blockin + breakgain)))
             format(ts, blockin, after, text.blanks(wd))
           else format(ts, blockin, after, text.newline.blanks(blockin + ind))
 
         case Str(s, len) :: ts => format(ts, blockin, after, text.string(s, len))
       }
     format(make_tree(input), 0, 0.0, Text()).content
   }
 
   def string_of(input: XML.Body,
       margin: Double = default_margin,
       breakgain: Double = default_breakgain,
       metric: Metric = Default_Metric): String =
     XML.content(formatted(input, margin = margin, breakgain = breakgain, metric = metric))
 }
diff --git a/src/Pure/term.scala b/src/Pure/term.scala
--- a/src/Pure/term.scala
+++ b/src/Pure/term.scala
@@ -1,228 +1,228 @@
 /*  Title:      Pure/term.scala
     Author:     Makarius
 
 Lambda terms, types, sorts.
 
 Note: Isabelle/ML is the primary environment for logical operations.
 */
 
 package isabelle
 
 
 object Term
 {
   /* types and terms */
 
   sealed case class Indexname(name: String, index: Int = 0)
   {
     override def toString: String =
       if (index == -1) name
       else {
         val dot =
           Symbol.explode(name).reverse match {
             case _ :: s :: _ if s == Symbol.sub_decoded || s == Symbol.sub => false
             case c :: _ => Symbol.is_digit(c)
             case _ => true
           }
         if (dot) "?" + name + "." + index
         else if (index != 0) "?" + name + index
         else "?" + name
       }
   }
 
   type Class = String
   type Sort = List[Class]
 
   sealed abstract class Typ
   case class Type(name: String, args: List[Typ] = Nil) extends Typ
   {
     override def toString: String =
       if (this == dummyT) "_"
       else "Type(" + name + (if (args.isEmpty) "" else "," + args) + ")"
   }
   case class TFree(name: String, sort: Sort = Nil) extends Typ
   {
     override def toString: String =
       "TFree(" + name + (if (sort.isEmpty) "" else "," + sort) + ")"
   }
   case class TVar(name: Indexname, sort: Sort = Nil) extends Typ
   {
     override def toString: String =
       "TVar(" + name + (if (sort.isEmpty) "" else "," + sort) + ")"
   }
   val dummyT: Type = Type("dummy")
 
   sealed abstract class Term
   {
     def head: Term =
       this match {
         case App(fun, _) => fun.head
         case _ => this
       }
   }
   case class Const(name: String, typargs: List[Typ] = Nil) extends Term
   {
     override def toString: String =
       if (this == dummy) "_"
       else "Const(" + name + (if (typargs.isEmpty) "" else "," + typargs) + ")"
   }
   case class Free(name: String, typ: Typ = dummyT) extends Term
   {
     override def toString: String =
       "Free(" + name + (if (typ == dummyT) "" else "," + typ) + ")"
   }
   case class Var(name: Indexname, typ: Typ = dummyT) extends Term
   {
     override def toString: String =
       "Var(" + name + (if (typ == dummyT) "" else "," + typ) + ")"
   }
   case class Bound(index: Int) extends Term
   case class Abs(name: String, typ: Typ, body: Term) extends Term
   case class App(fun: Term, arg: Term) extends Term
   {
     override def toString: String =
       this match {
         case OFCLASS(ty, c) => "OFCLASS(" + ty + "," + c + ")"
         case _ => "App(" + fun + "," + arg + ")"
       }
   }
 
   def dummy_pattern(ty: Typ): Term = Const("Pure.dummy_pattern", List(ty))
   val dummy: Term = dummy_pattern(dummyT)
 
   sealed abstract class Proof
   case object MinProof extends Proof
   case class PBound(index: Int) extends Proof
   case class Abst(name: String, typ: Typ, body: Proof) extends Proof
   case class AbsP(name: String, hyp: Term, body: Proof) extends Proof
   case class Appt(fun: Proof, arg: Term) extends Proof
   case class AppP(fun: Proof, arg: Proof) extends Proof
   case class Hyp(hyp: Term) extends Proof
   case class PAxm(name: String, types: List[Typ]) extends Proof
   case class PClass(typ: Typ, cls: Class) extends Proof
   case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof
   case class PThm(serial: Long, theory_name: String, name: String, types: List[Typ]) extends Proof
 
 
   /* type classes within the logic */
 
   object Class_Const
   {
     val suffix = "_class"
     def apply(c: Class): String = c + suffix
     def unapply(s: String): Option[Class] =
       if (s.endsWith(suffix)) Some(s.substring(0, s.length - suffix.length)) else None
   }
 
   object OFCLASS
   {
     def apply(ty: Typ, s: Sort): List[Term] = s.map(c => apply(ty, c))
 
     def apply(ty: Typ, c: Class): Term =
       App(Const(Class_Const(c), List(ty)), Const(Pure_Thy.TYPE, List(ty)))
 
     def unapply(t: Term): Option[(Typ, String)] =
       t match {
         case App(Const(Class_Const(c), List(ty)), Const(Pure_Thy.TYPE, List(ty1)))
         if ty == ty1 => Some((ty, c))
         case _ => None
       }
   }
 
 
 
   /** cache **/
 
   def make_cache(initial_size: Int = 131071, max_string: Int = Integer.MAX_VALUE): Cache =
     new Cache(initial_size, max_string)
 
   class Cache private[Term](initial_size: Int, max_string: Int)
     extends isabelle.Cache(initial_size, max_string)
   {
     protected def cache_indexname(x: Indexname): Indexname =
       lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index))
 
     protected def cache_sort(x: Sort): Sort =
       if (x.isEmpty) Nil else lookup(x) getOrElse store(x.map(cache_string))
 
     protected def cache_typ(x: Typ): Typ =
     {
       if (x == dummyT) dummyT
       else
         lookup(x) match {
           case Some(y) => y
           case None =>
             x match {
               case Type(name, args) => store(Type(cache_string(name), cache_typs(args)))
               case TFree(name, sort) => store(TFree(cache_string(name), cache_sort(sort)))
               case TVar(name, sort) => store(TVar(cache_indexname(name), cache_sort(sort)))
             }
         }
     }
 
     protected def cache_typs(x: List[Typ]): List[Typ] =
     {
       if (x.isEmpty) Nil
       else {
         lookup(x) match {
           case Some(y) => y
           case None => store(x.map(cache_typ))
         }
       }
     }
 
     protected def cache_term(x: Term): Term =
     {
       lookup(x) match {
         case Some(y) => y
         case None =>
           x match {
             case Const(name, typargs) => store(Const(cache_string(name), cache_typs(typargs)))
             case Free(name, typ) => store(Free(cache_string(name), cache_typ(typ)))
             case Var(name, typ) => store(Var(cache_indexname(name), cache_typ(typ)))
             case Bound(_) => store(x)
             case Abs(name, typ, body) =>
               store(Abs(cache_string(name), cache_typ(typ), cache_term(body)))
             case App(fun, arg) => store(App(cache_term(fun), cache_term(arg)))
           }
       }
     }
 
     protected def cache_proof(x: Proof): Proof =
     {
       if (x == MinProof) MinProof
       else {
         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)))
               case AbsP(name, hyp, body) =>
                 store(AbsP(cache_string(name), cache_term(hyp), cache_proof(body)))
               case Appt(fun, arg) => store(Appt(cache_proof(fun), cache_term(arg)))
               case AppP(fun, arg) => store(AppP(cache_proof(fun), cache_proof(arg)))
               case Hyp(hyp) => store(Hyp(cache_term(hyp)))
               case PAxm(name, types) => store(PAxm(cache_string(name), cache_typs(types)))
               case PClass(typ, cls) => store(PClass(cache_typ(typ), cache_string(cls)))
               case Oracle(name, prop, types) =>
                 store(Oracle(cache_string(name), cache_term(prop), cache_typs(types)))
               case PThm(serial, theory_name, name, types) =>
                 store(PThm(serial, cache_string(theory_name), cache_string(name), cache_typs(types)))
             }
         }
       }
     }
 
     // main methods
     def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) }
     def sort(x: Sort): Sort = synchronized { cache_sort(x) }
     def typ(x: Typ): Typ = synchronized { cache_typ(x) }
     def term(x: Term): Term = synchronized { cache_term(x) }
     def proof(x: Proof): Proof = synchronized { cache_proof(x) }
 
     def position(x: Position.T): Position.T =
       synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) }
   }
 }