# HG changeset patch
# User wenzelm
# Date 1147777286 -7200
# Node ID 213e12ad2c0328e88ba814354b7fded82c3e7ccd
# Parent  ea7162f8467756dbe9cf770ad36accd4b2ca31e5
added low-level string_of_term (back again from term.ML) -- should avoid this altogether;

diff -r ea7162f84677 -r 213e12ad2c03 src/HOL/Tools/ATP/recon_translate_proof.ML
--- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Tue May 16 13:01:24 2006 +0200
+++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Tue May 16 13:01:26 2006 +0200
@@ -65,7 +65,16 @@
     (ch = "~") orelse (ReconOrderClauses.is_alpha ch) orelse 
     (ReconOrderClauses.is_digit ch) orelse ( ch = " ");
 
-fun lit_string_with_nums t = let val termstr = Term.str_of_term t
+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 ^ ")"
+
+(* FIXME string_of_term is quite unreliable here *)
+fun lit_string_with_nums t = let val termstr = string_of_term t
                                  val exp_term = explode termstr
                              in
                                  implode(List.filter is_alpha_space_digit_or_neg exp_term)