# HG changeset patch
# User wenzelm
# Date 975611154 -3600
# Node ID a177b85710262b9885da8cdb0c153254b340285b
# Parent  ec9fab41b3a08d6995a5cc021387bdf56ebeba3c
added is_replaced_dummy_pattern;

diff -r ec9fab41b3a0 -r a177b8571026 src/Pure/term.ML
--- 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;