support dummy term;

--- a/src/Pure/term.scala	Thu Oct 17 21:03:59 2019 +0200
+++ b/src/Pure/term.scala	Thu Oct 17 21:31:53 2019 +0200
@@ -56,7 +56,8 @@
   case class Const(name: String, typargs: List[Typ] = Nil) extends Term
   {
     override def toString: String =
-      "Const(" + name + (if (typargs.isEmpty) "" else "," + typargs) + ")"
+      if (this == dummy) "_"
+      else "Const(" + name + (if (typargs.isEmpty) "" else "," + typargs) + ")"
   }
   case class Free(name: String, typ: Typ = dummyT) extends Term
   {
@@ -79,6 +80,9 @@
       }
   }
 
+  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