# HG changeset patch
# User wenzelm
# Date 1571340713 -7200
# Node ID 2cc7c05b3b3cb0efde6541001ab5ccc343c64f74
# Parent  8017d382a0d7b7b753afedab727ffdab7f965d7b
support dummy term;

diff -r 8017d382a0d7 -r 2cc7c05b3b3c src/Pure/term.scala
--- 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