src/HOL/Tools/sat_solver.ML
changeset 21268 7a6299a17386
parent 21267 5294ecae6708
child 21858 05f57309170c
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Thu Nov 09 18:48:45 2006 +0100
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Thu Nov 09 18:58:52 2006 +0100
     1.3 @@ -892,8 +892,7 @@
     1.4  					process_lines ls
     1.5  				)
     1.6  			(* proof *)
     1.7 -			val _ = tracing "process_lines"  (*TODO*)
     1.8 -			val _ = timeap process_lines proof_lines  (*TODO*)
     1.9 +			val _ = process_lines proof_lines
    1.10  			val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
    1.11  		in
    1.12  			SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id))