--- a/src/Pure/term.ML Fri Oct 07 18:49:19 2005 +0200
+++ b/src/Pure/term.ML Fri Oct 07 18:49:20 2005 +0200
@@ -210,6 +210,7 @@
val adhoc_freeze_vars: term -> term * string list
val string_of_vname: indexname -> string
val string_of_vname': indexname -> string
+ val str_of_term: term -> string
end;
structure Term: TERM =
@@ -1347,6 +1348,16 @@
fun string_of_vname' (x, ~1) = x
| string_of_vname' xi = string_of_vname xi;
+
+(* str_of_term *)
+
+fun str_of_term (Const (c, _)) = c
+ | str_of_term (Free (x, _)) = x
+ | str_of_term (Var (xi, _)) = string_of_vname xi
+ | str_of_term (Bound i) = string_of_int i
+ | str_of_term (Abs (x, _, t)) = "%" ^ x ^ ". " ^ str_of_term t
+ | str_of_term (t $ u) = "(" ^ str_of_term t ^ " " ^ str_of_term u ^ ")";
+
end;
structure BasicTerm: BASIC_TERM = Term;