added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
authorwenzelm
Fri Oct 07 18:49:20 2005 +0200 (2005-10-07)
changeset 1777705f5532a8289
parent 17776 4a518eec4a20
child 17778 93d7e524417a
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Fri Oct 07 18:49:19 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Fri Oct 07 18:49:20 2005 +0200
     1.3 @@ -210,6 +210,7 @@
     1.4    val adhoc_freeze_vars: term -> term * string list
     1.5    val string_of_vname: indexname -> string
     1.6    val string_of_vname': indexname -> string
     1.7 +  val str_of_term: term -> string
     1.8  end;
     1.9  
    1.10  structure Term: TERM =
    1.11 @@ -1347,6 +1348,16 @@
    1.12  fun string_of_vname' (x, ~1) = x
    1.13    | string_of_vname' xi = string_of_vname xi;
    1.14  
    1.15 +
    1.16 +(* str_of_term *)
    1.17 +
    1.18 +fun str_of_term (Const (c, _)) = c
    1.19 +  | str_of_term (Free (x, _)) = x
    1.20 +  | str_of_term (Var (xi, _)) = string_of_vname xi
    1.21 +  | str_of_term (Bound i) = string_of_int i
    1.22 +  | str_of_term (Abs (x, _, t)) = "%" ^ x ^ ". " ^ str_of_term t
    1.23 +  | str_of_term (t $ u) = "(" ^ str_of_term t ^ " " ^ str_of_term u ^ ")";
    1.24 +
    1.25  end;
    1.26  
    1.27  structure BasicTerm: BASIC_TERM = Term;