1.1 --- a/src/Pure/term.ML	Sun May 22 18:59:05 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Sun May 22 19:26:15 2005 +0200
     1.3 @@ -193,6 +193,7 @@
     1.4    val no_dummy_patterns: term -> term
     1.5    val replace_dummy_patterns: int * term -> int * term
     1.6    val is_replaced_dummy_pattern: indexname -> bool
     1.7 +  val show_dummy_patterns: term -> term
     1.8    val adhoc_freeze_vars: term -> term * string list
     1.9    val string_of_vname: indexname -> string
    1.10    val string_of_vname': indexname -> string
    1.11 @@ -1103,6 +1104,11 @@
    1.12  fun is_replaced_dummy_pattern ("_dummy_", _) = true
    1.13    | is_replaced_dummy_pattern _ = false;
    1.14  
    1.15 +fun show_dummy_patterns (Var (("_dummy_", _), T)) = Const ("dummy_pattern", T)
    1.16 +  | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u
    1.17 +  | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t)
    1.18 +  | show_dummy_patterns a = a;
    1.19 +
    1.20  
    1.21  (* adhoc freezing *)
    1.22