diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Thu Aug 19 11:02:14 2010 +0200
@@ -217,7 +217,7 @@
 	(* Thm.cterm -> int option *)
 	fun index_of_literal chyp = (
 		case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
-		  (Const ("Not", _) $ atom) =>
+		  (Const (@{const_name "Not"}, _) $ atom) =>
 			SOME (~ (the (Termtab.lookup atom_table atom)))
 		| atom =>
 			SOME (the (Termtab.lookup atom_table atom))