added string_of_term
authornipkow
Thu Mar 17 12:19:50 2005 +0100 (2005-03-17 ago)
changeset 15612431b281078b3
parent 15611 c01f11cd08f9
child 15613 ab90e95ae02e
added string_of_term
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Thu Mar 17 01:40:18 2005 +0100
     1.2 +++ b/src/Pure/term.ML	Thu Mar 17 12:19:50 2005 +0100
     1.3 @@ -195,6 +195,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 string_of_term: term -> string
     1.8  end;
     1.9  
    1.10  structure Term: TERM =
    1.11 @@ -1132,6 +1133,14 @@
    1.12  fun string_of_vname' (x, ~1) = x
    1.13    | string_of_vname' xi = string_of_vname xi;
    1.14  
    1.15 +fun string_of_term (Const(s,_)) = s
    1.16 +  | string_of_term (Free(s,_)) = s
    1.17 +  | string_of_term (Var(ix,_)) = string_of_vname ix
    1.18 +  | string_of_term (Bound i) = string_of_int i
    1.19 +  | string_of_term (Abs(x,_,t)) = "%" ^ x ^ ". " ^ string_of_term t
    1.20 +  | string_of_term (s $ t) =
    1.21 +      "(" ^ string_of_term s ^ " " ^ string_of_term t ^ ")"
    1.22 +
    1.23  end;
    1.24  
    1.25  structure BasicTerm: BASIC_TERM = Term;