src/HOL/ex/SAT_Examples.thy
changeset 42012 2c3fe3cbebae
parent 41471 54a58904a598
child 47432 e1576d13e933
     1.1 --- a/src/HOL/ex/SAT_Examples.thy	Sun Mar 20 21:20:07 2011 +0100
     1.2 +++ b/src/HOL/ex/SAT_Examples.thy	Sun Mar 20 21:28:11 2011 +0100
     1.3 @@ -536,13 +536,12 @@
     1.4    fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc)
     1.5      | and_to_list fm acc = rev (fm :: acc)
     1.6    val clauses = and_to_list prop_fm []
     1.7 -  val terms   = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula)
     1.8 -    clauses
     1.9 -  val cterms  = map (Thm.cterm_of @{theory}) terms
    1.10 -  val timer   = start_timing ()
    1.11 -  val thm     = sat.rawsat_thm @{context} cterms
    1.12 +  val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
    1.13 +  val cterms = map (Thm.cterm_of @{theory}) terms
    1.14 +  val start = Timing.start ()
    1.15 +  val thm = sat.rawsat_thm @{context} cterms
    1.16  in
    1.17 -  (end_timing timer, !sat.counter)
    1.18 +  (Timing.result start, ! sat.counter)
    1.19  end;
    1.20  *}
    1.21