diff -r bcd14373ec30 -r 64f30bdd3ba1 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Fri Aug 28 18:23:24 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Fri Aug 28 21:04:03 2009 +0200
@@ -51,7 +51,7 @@
 	val trace_sat: bool ref    (* input: print trace messages *)
 	val solver: string ref  (* input: name of SAT solver to be used *)
 	val counter: int ref     (* output: number of resolution steps during last proof replay *)
-	val rawsat_thm: cterm list -> thm
+	val rawsat_thm: Proof.context -> cterm list -> thm
 	val rawsat_tac: Proof.context -> int -> tactic
 	val sat_tac: Proof.context -> int -> tactic
 	val satx_tac: Proof.context -> int -> tactic
@@ -295,9 +295,7 @@
 (*      hyps).                                                               *)
 (* ------------------------------------------------------------------------- *)
 
-(* Thm.cterm list -> Thm.thm *)
-
-fun rawsat_thm clauses =
+fun rawsat_thm ctxt clauses =
 let
 	(* remove premises that equal "True" *)
 	val clauses' = filter (fn clause =>
@@ -310,7 +308,7 @@
 		((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause
 			handle TERM ("dest_Trueprop", _) => false)
 		orelse (
-			warning ("Ignoring non-clausal premise " ^ Display.string_of_cterm clause);
+			warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause));
 			false)) clauses'
 	(* remove trivial clauses -- this is necessary because zChaff removes *)
 	(* trivial clauses during preprocessing, and otherwise our clause     *)
@@ -323,7 +321,8 @@
 	(* sorted in ascending order                                          *)
 	val sorted_clauses = sort (TermOrd.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
 	val _ = if !trace_sat then
-			tracing ("Sorted non-trivial clauses:\n" ^ cat_lines (map Display.string_of_cterm sorted_clauses))
+			tracing ("Sorted non-trivial clauses:\n" ^
+			  cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
 		else ()
 	(* translate clauses from HOL terms to PropLogic.prop_formula *)
 	val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) sorted_clauses Termtab.empty
@@ -411,7 +410,8 @@
 (* ------------------------------------------------------------------------- *)
 
 fun rawsat_tac ctxt i =
-  Subgoal.FOCUS (fn {prems, ...} => rtac (rawsat_thm (map cprop_of prems)) 1) ctxt i;
+  Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
+    rtac (rawsat_thm ctxt' (map cprop_of prems)) 1) ctxt i;
 
 (* ------------------------------------------------------------------------- *)
 (* pre_cnf_tac: converts the i-th subgoal                                    *)