src/HOL/Tools/sat_funcs.ML
changeset 32155 e2bf2f73b0c8
parent 32091 30e2ffbba718
child 32231 95b8afcbb0ed
     1.1 --- a/src/HOL/Tools/sat_funcs.ML	Thu Jul 23 22:20:37 2009 +0200
     1.2 +++ b/src/HOL/Tools/sat_funcs.ML	Thu Jul 23 23:12:21 2009 +0200
     1.3 @@ -337,7 +337,7 @@
     1.4  		val _ = if !trace_sat then
     1.5  				tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
     1.6  			else ()
     1.7 -		val False_thm = SkipProof.make_thm (the_context ()) (HOLogic.Trueprop $ HOLogic.false_const)
     1.8 +		val False_thm = SkipProof.make_thm @{theory} (HOLogic.Trueprop $ HOLogic.false_const)
     1.9  	in
    1.10  		(* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold    *)
    1.11  		(* Thm.weaken sorted_clauses' would be quadratic, since we sorted   *)
    1.12 @@ -388,7 +388,7 @@
    1.13  			val msg = "SAT solver found a countermodel:\n"
    1.14  				^ (commas
    1.15  					o map (fn (term, idx) =>
    1.16 -						Syntax.string_of_term_global (the_context ()) term ^ ": "
    1.17 +						Syntax.string_of_term_global @{theory} term ^ ": "
    1.18  							^ (case assignment idx of NONE => "arbitrary" | SOME true => "true" | SOME false => "false")))
    1.19  					(Termtab.dest atom_table)
    1.20  		in