src/Pure/term.ML

   val dummy_prop: term
   val is_dummy_pattern: term -> bool
   val free_dummy_patterns: term -> Name.context -> term * Name.context
   val no_dummy_patterns: term -> term
   val replace_dummy_patterns: term -> int -> term * int
-  val is_replaced_dummy_pattern: indexname -> bool
   val show_dummy_patterns: term -> term
   val string_of_vname: indexname -> string
   val string_of_vname': indexname -> string
 end;
 

       in (t' $ u', i'') end
   | replace_dummy _ a i = (a, i);
 
 val replace_dummy_patterns = replace_dummy [];
 
-fun is_replaced_dummy_pattern ("_dummy_", _) = true
-  | is_replaced_dummy_pattern _ = false;
-
 fun show_dummy_patterns (Var (("_dummy_", _), T)) = 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;