--- a/src/HOL/Tools/ATP/recon_translate_proof.ML Fri Oct 07 17:57:21 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Fri Oct 07 18:49:19 2005 +0200
@@ -65,15 +65,7 @@
(ch = "~") orelse (ReconOrderClauses.is_alpha ch) orelse
(ReconOrderClauses.is_digit ch) orelse ( ch = " ");
-fun string_of_term (Const(s,_)) = s
- | string_of_term (Free(s,_)) = s
- | string_of_term (Var(ix,_)) = Term.string_of_vname ix
- | string_of_term (Bound i) = string_of_int i
- | string_of_term (Abs(x,_,t)) = "%" ^ x ^ ". " ^ string_of_term t
- | string_of_term (s $ t) =
- "(" ^ string_of_term s ^ " " ^ string_of_term t ^ ")"
-
-fun lit_string_with_nums t = let val termstr = string_of_term t
+fun lit_string_with_nums t = let val termstr = Term.str_of_term t
val exp_term = explode termstr
in
implode(List.filter is_alpha_space_digit_or_neg exp_term)