diff -r 9926c47ad1a1 -r 32ad17fe2b9c src/HOL/Tools/prop_logic.ML
--- a/src/HOL/Tools/prop_logic.ML	Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/prop_logic.ML	Thu Aug 19 16:08:59 2010 +0200
@@ -391,11 +391,11 @@
 				next_idx_is_valid := true;
 				Unsynchronized.inc next_idx
 			)
-		fun aux (Const (@{const_name "True"}, _))         table =
+		fun aux (Const (@{const_name True}, _))         table =
 			(True, table)
-		  | aux (Const (@{const_name "False"}, _))        table =
+		  | aux (Const (@{const_name False}, _))        table =
 			(False, table)
-		  | aux (Const (@{const_name "Not"}, _) $ x)      table =
+		  | aux (Const (@{const_name Not}, _) $ x)      table =
 			apfst Not (aux x table)
 		  | aux (Const (@{const_name "op |"}, _) $ x $ y) table =
 			let