added is_replaced_dummy_pattern;

--- a/src/Pure/term.ML	Thu Nov 30 20:05:34 2000 +0100
+++ b/src/Pure/term.ML	Thu Nov 30 20:05:54 2000 +0100
@@ -182,6 +182,7 @@
   val dummy_patternN: string
   val no_dummy_patterns: term -> term
   val replace_dummy_patterns: int * term -> int * term
+  val is_replaced_dummy_pattern: indexname -> bool
 end;
 
 structure Term: TERM =
@@ -1073,6 +1074,8 @@
 val replace_dummy_patterns = foldl_map_aterms (fn (i, t) =>
   if is_dummy_pattern t then (i + 1, Var (("_dummy_", i), fastype_of t)) else (i, t));
 
+fun is_replaced_dummy_pattern ("_dummy_", _) = true
+  | is_replaced_dummy_pattern _ = false;
 
 end;