src/HOL/Tools/sat_funcs.ML

 fun replay_proof atom_table clauses (clause_table, empty_id) =
 let
 	(* 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))
 	) handle TERM _ => NONE;  (* 'chyp' is not a literal *)