| changeset 7318 | 768fab6dae74 |
| parent 6963 | 6109bcedbe1a |
| child 7406 | e94cbbe72c5d |
--- 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;