src/HOL/Tools/res_clause.ML
changeset 22130 0906fd95e0b5
parent 22079 b161604f0c8d
child 22383 01e90256550d
     1.1 --- a/src/HOL/Tools/res_clause.ML	Sat Jan 20 14:09:12 2007 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Sat Jan 20 14:09:14 2007 +0100
     1.3 @@ -425,7 +425,7 @@
     1.4  fun make_axiom_clause thm (ax_name,cls_id) =
     1.5    if Meson.is_fol_term (prop_of thm) 
     1.6    then (SOME (make_clause(cls_id, ax_name, thm, Axiom)) handle MAKE_CLAUSE => NONE)
     1.7 -  else (Output.debug ("Omitting " ^ ax_name ^ ": Axiom is not FOL"); NONE)
     1.8 +  else (Output.debug (fn () => ("Omitting " ^ ax_name ^ ": Axiom is not FOL")); NONE)
     1.9      
    1.10  fun make_axiom_clauses [] = []
    1.11    | make_axiom_clauses ((thm,(name,id))::thms) =
    1.12 @@ -732,7 +732,7 @@
    1.13  (* write out a subgoal in DFG format to the file "xxxx_N"*)
    1.14  fun dfg_write_file thms filename (ax_tuples,classrel_clauses,arity_clauses) = 
    1.15    let 
    1.16 -    val _ = Output.debug ("Preparing to write the DFG file " ^ filename)
    1.17 +    val _ = Output.debug (fn () => ("Preparing to write the DFG file " ^ filename))
    1.18      val conjectures = make_conjecture_clauses thms
    1.19      val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples)
    1.20      val (dfg_clss, tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
    1.21 @@ -818,7 +818,7 @@
    1.22  (* write out a subgoal as tptp clauses to the file "xxxx_N"*)
    1.23  fun tptp_write_file thms filename (ax_tuples,classrel_clauses,arity_clauses) =
    1.24    let
    1.25 -    val _ = Output.debug ("Preparing to write the TPTP file " ^ filename)
    1.26 +    val _ = Output.debug (fn () => ("Preparing to write the TPTP file " ^ filename))
    1.27      val clss = make_conjecture_clauses thms
    1.28      val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples)
    1.29      val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss)