diff -r ece660815e03 -r 768fab6dae74 src/Pure/term.ML
--- a/src/Pure/term.ML	Sun Aug 22 21:14:44 1999 +0200
+++ b/src/Pure/term.ML	Mon Aug 23 09:36:05 1999 +0200
@@ -37,6 +37,7 @@
     $ of term * term
   exception TYPE of string * typ list * term list
   exception TERM of string * term list
+  val is_Bound: term -> bool
   val is_Const: term -> bool
   val is_Free: term -> bool
   val is_Var: term -> bool
@@ -241,6 +242,9 @@
 
 (** Discriminators **)
 
+fun is_Bound (Bound _) = true
+  | is_Bound _         = false;
+
 fun is_Const (Const _) = true
   | is_Const _ = false;