# HG changeset patch
# User wenzelm
# Date 1433965742 -7200
# Node ID be7565a1115b90b9f8ba8553bbe10fa2634eede6
# Parent  92d9557fb78c2308ce02232ec551d6e21ec8baa9
unused;

diff -r 92d9557fb78c -r be7565a1115b src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Jun 10 20:15:58 2015 +0200
+++ b/src/Pure/term.ML	Wed Jun 10 21:49:02 2015 +0200
@@ -167,7 +167,6 @@
   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
@@ -966,9 +965,6 @@
 
 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)