src/Pure/term.ML

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