diff -r 39acf19e9f3a -r 30e2ffbba718 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Tue Jul 21 01:03:18 2009 +0200
@@ -119,7 +119,7 @@
 (* (Thm.thm * (int * Thm.cterm) list) list -> Thm.thm * (int * Thm.cterm) list *)
 
 fun resolve_raw_clauses [] =
-	raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
+      raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
   | resolve_raw_clauses (c::cs) =
 	let
 		(* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *)
@@ -134,9 +134,9 @@
 		(* find out which two hyps are used in the resolution *)
 		(* (int * Thm.cterm) list * (int * Thm.cterm) list -> (int * Thm.cterm) list -> bool * Thm.cterm * Thm.cterm * (int * Thm.cterm) list *)
 		fun find_res_hyps ([], _) _ =
-			raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
+          raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
 		  | find_res_hyps (_, []) _ =
-			raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
+          raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
 		  | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc =
 			(case (lit_ord o pairself fst) (h1, h2) of
 			  LESS  => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc)
@@ -154,9 +154,12 @@
 		(* Thm.thm * (int * Thm.cterm) list -> Thm.thm * (int * Thm.cterm) list -> Thm.thm * (int * Thm.cterm) list *)
 		fun resolution (c1, hyps1) (c2, hyps2) =
 		let
-			val _ = if !trace_sat then
-					tracing ("Resolving clause: " ^ Display.string_of_thm c1 ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1))
-						^ ")\nwith clause: " ^ Display.string_of_thm c2 ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
+			val _ =
+			  if ! trace_sat then
+					tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^
+					  " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1))
+						^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^
+						" (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
 				else ()
 
 			(* the two literals used for resolution *)
@@ -172,8 +175,9 @@
 					Thm.instantiate ([], [(cP, cLit)]) resolution_thm
 				end
 
-			val _ = if !trace_sat then
-					tracing ("Resolution theorem: " ^ Display.string_of_thm res_thm)
+			val _ =
+			  if !trace_sat then
+					tracing ("Resolution theorem: " ^ Display.string_of_thm_without_context res_thm)
 				else ()
 
 			(* Gamma1, Gamma2 |- False *)
@@ -181,8 +185,11 @@
 				(Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1'))
 				(if hyp1_is_neg then c1' else c2')
 
-			val _ = if !trace_sat then
-					tracing ("Resulting clause: " ^ Display.string_of_thm c_new ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
+			val _ =
+			  if !trace_sat then
+					tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^
+					  " (hyps: " ^ ML_Syntax.print_list
+					      (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
 				else ()
 			val _ = inc counter
 		in