src/HOL/Tools/res_atp.ML
changeset 19746 9ac97dc14214
parent 19744 73aab222fecb
child 19768 9afd9b9c47d0
     1.1 --- a/src/HOL/Tools/res_atp.ML	Mon May 29 17:38:02 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Mon May 29 17:38:30 2006 +0200
     1.3 @@ -207,7 +207,7 @@
     1.4  			  else fn_lg f (FOL,seen)
     1.5  	val _ =
     1.6            if is_fol_logic lg' then ()
     1.7 -          else warning ("Found a HOL term: " ^ Display.raw_string_of_term f)
     1.8 +          else Output.debug ("Found a HOL term: " ^ Display.raw_string_of_term f)
     1.9  	 in
    1.10  	     term_lg (args@tms) (lg',seen')
    1.11      end
    1.12 @@ -230,7 +230,7 @@
    1.13  			  else pred_lg pred (lg,seen)
    1.14  	val _ =
    1.15            if is_fol_logic lg' then ()
    1.16 -          else warning ("Found a HOL predicate: " ^ Display.raw_string_of_term pred)
    1.17 +          else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred)
    1.18      in
    1.19  	term_lg args (lg',seen')
    1.20      end;
    1.21 @@ -240,7 +240,7 @@
    1.22      let val (lg,seen') = lit_lg lit (FOL,seen)
    1.23  	val _ =
    1.24            if is_fol_logic lg then ()
    1.25 -          else warning ("Found a HOL literal: " ^ Display.raw_string_of_term lit)
    1.26 +          else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit)
    1.27      in
    1.28  	lits_lg lits (lg,seen')
    1.29      end
    1.30 @@ -265,7 +265,7 @@
    1.31      let val (lg,seen') = logic_of_clause cls (FOL,seen)
    1.32  	val _ =
    1.33            if is_fol_logic lg then ()
    1.34 -          else warning ("Found a HOL clause: " ^ Display.raw_string_of_term cls)
    1.35 +          else Output.debug ("Found a HOL clause: " ^ Display.raw_string_of_term cls)
    1.36      in
    1.37  	logic_of_clauses clss (lg,seen')
    1.38      end
    1.39 @@ -325,16 +325,16 @@
    1.40  	val file = atp_input_file()
    1.41      in
    1.42  	(writer prob_logic goal_cls file (axclauses_as_thms,classrel_clauses,arity_clauses);
    1.43 -	 warning ("Writing to " ^ file);
    1.44 +	 Output.debug ("Writing to " ^ file);
    1.45  	 file)
    1.46      end;
    1.47  
    1.48  
    1.49  (**** remove tmp files ****)
    1.50  fun cond_rm_tmp file = 
    1.51 -    if !keep_atp_input then warning "ATP input kept..." 
    1.52 -    else if !destdir <> "" then warning ("ATP input kept in directory " ^ (!destdir))
    1.53 -    else (warning "deleting ATP inputs..."; OS.FileSys.remove file);
    1.54 +    if !keep_atp_input then Output.debug "ATP input kept..." 
    1.55 +    else if !destdir <> "" then Output.debug ("ATP input kept in directory " ^ (!destdir))
    1.56 +    else (Output.debug "deleting ATP inputs..."; OS.FileSys.remove file);
    1.57  
    1.58  
    1.59  (****** setup ATPs as Isabelle methods ******)