--- 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 *)