# HG changeset patch
# User wenzelm
# Date 1147777290 -7200
# Node ID 043921b0e587ce80d3045c7f196234108b0844c4
# Parent  91c0ae7e542b0784e185a6456de4a64e885912e8
removed low-level str_of_sort/typ/term (use Display.raw_string_of_sort/typ/term instead, or even PolyML.print -- for debugging purposes);

diff -r 91c0ae7e542b -r 043921b0e587 src/Pure/term.ML
--- a/src/Pure/term.ML	Tue May 16 13:01:29 2006 +0200
+++ b/src/Pure/term.ML	Tue May 16 13:01:30 2006 +0200
@@ -209,9 +209,6 @@
   val adhoc_freeze_vars: term -> term * string list
   val string_of_vname: indexname -> string
   val string_of_vname': indexname -> string
-  val str_of_sort: sort -> string
-  val str_of_typ: typ -> string
-  val str_of_term: term -> string
 end;
 
 structure Term: TERM =
@@ -1335,37 +1332,6 @@
 fun string_of_vname' (x, ~1) = x
   | string_of_vname' xi = string_of_vname xi;
 
-fun str_of_sort [] = "{}"
-  | str_of_sort [c] = c
-  | str_of_sort cs = (enclose "{" "}" o commas) cs
-
-fun str_of_typ (Type ("fun", [ty1, ty2])) =
-      "(" ^ str_of_typ ty1 ^ " => " ^ str_of_typ ty2 ^ ")"
-  | str_of_typ (Type ("dummy", [])) =
-      "_"
-  | str_of_typ (Type (tyco, _)) =
-      tyco
-  | str_of_typ (Type (tyco, tys)) =
-      (enclose "(" ")" o space_implode " ") (tyco :: map str_of_typ tys)
-  | str_of_typ (TFree (v, sort)) =
-      v ^ "::" ^ str_of_sort sort
-  | str_of_typ (TVar (vi, sort)) =
-      string_of_vname vi ^ "::" ^ str_of_sort sort;
-
-val str_of_term =
-  let
-    fun typed (s, ty) = s ^ "::" ^ str_of_typ ty;
-    fun bound vs i = case AList.lookup (op =) vs i
-     of SOME v => enclose "[" "]" (string_of_int i ^ " ~> " ^ v)
-      | NONE => (enclose "[" "]" o string_of_int) i
-    fun str vs (Const (c, _)) = c
-      | str vs (Free (v, ty)) = typed (v, ty)
-      | str vs (Var (vi, ty)) = typed (string_of_vname vi, ty)
-      | str vs (Bound i) = bound vs i
-      | str vs (Abs (x, ty, t)) = "(%" ^ typed (x, ty) ^ ". " ^ str ((length vs, x)::vs) t ^ ")"
-      | str vs (t1 $ t2) = "(" ^ str vs t1 ^ " " ^ str vs t2 ^ ")";
-  in str [] end;
-
 end;
 
 structure BasicTerm: BASIC_TERM = Term;