# HG changeset patch
# User wenzelm
# Date 1128703760 -7200
# Node ID 05f5532a8289bc84b6f2a9bdd13f9e04126259b7
# Parent  4a518eec4a2078f6a4cd5205eb5fb287d486f373
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);

diff -r 4a518eec4a20 -r 05f5532a8289 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;