# HG changeset patch
# User nipkow
# Date 1111058390 -3600
# Node ID 431b281078b354fb6b0696f5896bd22c24d59790
# Parent  c01f11cd08f9b65b48c5f7bd96c5f1e4067f2a25
added string_of_term

diff -r c01f11cd08f9 -r 431b281078b3 src/Pure/term.ML
--- a/src/Pure/term.ML	Thu Mar 17 01:40:18 2005 +0100
+++ b/src/Pure/term.ML	Thu Mar 17 12:19:50 2005 +0100
@@ -195,6 +195,7 @@
   val adhoc_freeze_vars: term -> term * string list
   val string_of_vname: indexname -> string
   val string_of_vname': indexname -> string
+  val string_of_term: term -> string
 end;
 
 structure Term: TERM =
@@ -1132,6 +1133,14 @@
 fun string_of_vname' (x, ~1) = x
   | string_of_vname' xi = string_of_vname xi;
 
+fun string_of_term (Const(s,_)) = s
+  | string_of_term (Free(s,_)) = s
+  | string_of_term (Var(ix,_)) = string_of_vname ix
+  | string_of_term (Bound i) = string_of_int i
+  | string_of_term (Abs(x,_,t)) = "%" ^ x ^ ". " ^ string_of_term t
+  | string_of_term (s $ t) =
+      "(" ^ string_of_term s ^ " " ^ string_of_term t ^ ")"
+
 end;
 
 structure BasicTerm: BASIC_TERM = Term;