# HG changeset patch
# User wenzelm
# Date 1116782775 -7200
# Node ID 31bd65f7b22ac287293c6fd29ecdcafa0d1abad8
# Parent  6ccd552ee3665bc3445fdc05b0b6a4440d9fe284
added show_dummy_patterns;

diff -r 6ccd552ee366 -r 31bd65f7b22a src/Pure/term.ML
--- a/src/Pure/term.ML	Sun May 22 18:59:05 2005 +0200
+++ b/src/Pure/term.ML	Sun May 22 19:26:15 2005 +0200
@@ -193,6 +193,7 @@
   val no_dummy_patterns: term -> term
   val replace_dummy_patterns: int * term -> int * term
   val is_replaced_dummy_pattern: indexname -> bool
+  val show_dummy_patterns: term -> term
   val adhoc_freeze_vars: term -> term * string list
   val string_of_vname: indexname -> string
   val string_of_vname': indexname -> string
@@ -1103,6 +1104,11 @@
 fun is_replaced_dummy_pattern ("_dummy_", _) = true
   | is_replaced_dummy_pattern _ = false;
 
+fun show_dummy_patterns (Var (("_dummy_", _), T)) = Const ("dummy_pattern", T)
+  | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u
+  | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t)
+  | show_dummy_patterns a = a;
+
 
 (* adhoc freezing *)