src/HOL/Tools/res_atp.ML
changeset 19641 f1de44e61ec1
parent 19617 7cb4b67d4b97
child 19675 a4894fb2a5f2
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue May 16 13:01:22 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue May 16 13:01:23 2006 +0200
     1.3 @@ -194,7 +194,9 @@
     1.4      let val (f,args) = strip_comb tm
     1.5  	val (lg',seen') = if f mem seen then (FOL,seen) 
     1.6  			  else fn_lg f (FOL,seen)
     1.7 -	val _ = if is_fol_logic lg' then () else warning ("Found a HOL term: " ^ (Term.str_of_term f))
     1.8 +	val _ =
     1.9 +          if is_fol_logic lg' then ()
    1.10 +          else warning ("Found a HOL term: " ^ Display.raw_string_of_term f)
    1.11  	 in
    1.12  	     term_lg (args@tms) (lg',seen')
    1.13      end
    1.14 @@ -215,7 +217,9 @@
    1.15      let val (pred,args) = strip_comb P
    1.16  	val (lg',seen') = if pred mem seen then (lg,seen) 
    1.17  			  else pred_lg pred (lg,seen)
    1.18 -	val _ = if is_fol_logic lg' then () else warning ("Found a HOL predicate: " ^ (Term.str_of_term pred))
    1.19 +	val _ =
    1.20 +          if is_fol_logic lg' then ()
    1.21 +          else warning ("Found a HOL predicate: " ^ Display.raw_string_of_term pred)
    1.22      in
    1.23  	term_lg args (lg',seen')
    1.24      end;
    1.25 @@ -223,7 +227,9 @@
    1.26  fun lits_lg [] (lg,seen) = (lg,seen)
    1.27    | lits_lg (lit::lits) (FOL,seen) =
    1.28      let val (lg,seen') = lit_lg lit (FOL,seen)
    1.29 -	val _ =  if is_fol_logic lg then () else warning ("Found a HOL literal: " ^ (Term.str_of_term lit))
    1.30 +	val _ =
    1.31 +          if is_fol_logic lg then ()
    1.32 +          else warning ("Found a HOL literal: " ^ Display.raw_string_of_term lit)
    1.33      in
    1.34  	lits_lg lits (lg,seen')
    1.35      end
    1.36 @@ -246,7 +252,9 @@
    1.37  fun logic_of_clauses [] (lg,seen) = (lg,seen)
    1.38    | logic_of_clauses (cls::clss) (FOL,seen) =
    1.39      let val (lg,seen') = logic_of_clause cls (FOL,seen)
    1.40 -	val _ = if is_fol_logic lg then () else warning ("Found a HOL clause: " ^ (Term.str_of_term cls))
    1.41 +	val _ =
    1.42 +          if is_fol_logic lg then ()
    1.43 +          else warning ("Found a HOL clause: " ^ Display.raw_string_of_term cls)
    1.44      in
    1.45  	logic_of_clauses clss (lg,seen')
    1.46      end