--- 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)