# HG changeset patch
# User wenzelm
# Date 1147777283 -7200
# Node ID f1de44e61ec11858ace6ea761a5100fad9fb9b8d
# Parent  40ec8931742556904dbf3e92535ce9845c027dc0
replaced low-level Term.str_of by Display.raw_string_of_term (should actually use Display.string_of_term);

diff -r 40ec89317425 -r f1de44e61ec1 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Tue May 16 13:01:22 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Tue May 16 13:01:23 2006 +0200
@@ -194,7 +194,9 @@
     let val (f,args) = strip_comb tm
 	val (lg',seen') = if f mem seen then (FOL,seen) 
 			  else fn_lg f (FOL,seen)
-	val _ = if is_fol_logic lg' then () else warning ("Found a HOL term: " ^ (Term.str_of_term f))
+	val _ =
+          if is_fol_logic lg' then ()
+          else warning ("Found a HOL term: " ^ Display.raw_string_of_term f)
 	 in
 	     term_lg (args@tms) (lg',seen')
     end
@@ -215,7 +217,9 @@
     let val (pred,args) = strip_comb P
 	val (lg',seen') = if pred mem seen then (lg,seen) 
 			  else pred_lg pred (lg,seen)
-	val _ = if is_fol_logic lg' then () else warning ("Found a HOL predicate: " ^ (Term.str_of_term pred))
+	val _ =
+          if is_fol_logic lg' then ()
+          else warning ("Found a HOL predicate: " ^ Display.raw_string_of_term pred)
     in
 	term_lg args (lg',seen')
     end;
@@ -223,7 +227,9 @@
 fun lits_lg [] (lg,seen) = (lg,seen)
   | lits_lg (lit::lits) (FOL,seen) =
     let val (lg,seen') = lit_lg lit (FOL,seen)
-	val _ =  if is_fol_logic lg then () else warning ("Found a HOL literal: " ^ (Term.str_of_term lit))
+	val _ =
+          if is_fol_logic lg then ()
+          else warning ("Found a HOL literal: " ^ Display.raw_string_of_term lit)
     in
 	lits_lg lits (lg,seen')
     end
@@ -246,7 +252,9 @@
 fun logic_of_clauses [] (lg,seen) = (lg,seen)
   | logic_of_clauses (cls::clss) (FOL,seen) =
     let val (lg,seen') = logic_of_clause cls (FOL,seen)
-	val _ = if is_fol_logic lg then () else warning ("Found a HOL clause: " ^ (Term.str_of_term cls))
+	val _ =
+          if is_fol_logic lg then ()
+          else warning ("Found a HOL clause: " ^ Display.raw_string_of_term cls)
     in
 	logic_of_clauses clss (lg,seen')
     end