src/Pure/term.ML
changeset 19647 043921b0e587
parent 19473 d87a8838afa4
child 19909 6b5574d64aa4
     1.1 --- a/src/Pure/term.ML	Tue May 16 13:01:29 2006 +0200
     1.2 +++ b/src/Pure/term.ML	Tue May 16 13:01:30 2006 +0200
     1.3 @@ -209,9 +209,6 @@
     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_sort: sort -> string
     1.8 -  val str_of_typ: typ -> string
     1.9 -  val str_of_term: term -> string
    1.10  end;
    1.11  
    1.12  structure Term: TERM =
    1.13 @@ -1335,37 +1332,6 @@
    1.14  fun string_of_vname' (x, ~1) = x
    1.15    | string_of_vname' xi = string_of_vname xi;
    1.16  
    1.17 -fun str_of_sort [] = "{}"
    1.18 -  | str_of_sort [c] = c
    1.19 -  | str_of_sort cs = (enclose "{" "}" o commas) cs
    1.20 -
    1.21 -fun str_of_typ (Type ("fun", [ty1, ty2])) =
    1.22 -      "(" ^ str_of_typ ty1 ^ " => " ^ str_of_typ ty2 ^ ")"
    1.23 -  | str_of_typ (Type ("dummy", [])) =
    1.24 -      "_"
    1.25 -  | str_of_typ (Type (tyco, _)) =
    1.26 -      tyco
    1.27 -  | str_of_typ (Type (tyco, tys)) =
    1.28 -      (enclose "(" ")" o space_implode " ") (tyco :: map str_of_typ tys)
    1.29 -  | str_of_typ (TFree (v, sort)) =
    1.30 -      v ^ "::" ^ str_of_sort sort
    1.31 -  | str_of_typ (TVar (vi, sort)) =
    1.32 -      string_of_vname vi ^ "::" ^ str_of_sort sort;
    1.33 -
    1.34 -val str_of_term =
    1.35 -  let
    1.36 -    fun typed (s, ty) = s ^ "::" ^ str_of_typ ty;
    1.37 -    fun bound vs i = case AList.lookup (op =) vs i
    1.38 -     of SOME v => enclose "[" "]" (string_of_int i ^ " ~> " ^ v)
    1.39 -      | NONE => (enclose "[" "]" o string_of_int) i
    1.40 -    fun str vs (Const (c, _)) = c
    1.41 -      | str vs (Free (v, ty)) = typed (v, ty)
    1.42 -      | str vs (Var (vi, ty)) = typed (string_of_vname vi, ty)
    1.43 -      | str vs (Bound i) = bound vs i
    1.44 -      | str vs (Abs (x, ty, t)) = "(%" ^ typed (x, ty) ^ ". " ^ str ((length vs, x)::vs) t ^ ")"
    1.45 -      | str vs (t1 $ t2) = "(" ^ str vs t1 ^ " " ^ str vs t2 ^ ")";
    1.46 -  in str [] end;
    1.47 -
    1.48  end;
    1.49  
    1.50  structure BasicTerm: BASIC_TERM = Term;