diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/prop_logic.ML
--- a/src/HOL/Tools/prop_logic.ML	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/prop_logic.ML	Fri Aug 27 10:56:46 2010 +0200
@@ -397,14 +397,14 @@
 			(False, table)
 		  | aux (Const (@{const_name Not}, _) $ x)      table =
 			apfst Not (aux x table)
-		  | aux (Const (@{const_name "op |"}, _) $ x $ y) table =
+		  | aux (Const (@{const_name HOL.disj}, _) $ x $ y) table =
 			let
 				val (fm1, table1) = aux x table
 				val (fm2, table2) = aux y table1
 			in
 				(Or (fm1, fm2), table2)
 			end
-		  | aux (Const (@{const_name "op &"}, _) $ x $ y) table =
+		  | aux (Const (@{const_name HOL.conj}, _) $ x $ y) table =
 			let
 				val (fm1, table1) = aux x table
 				val (fm2, table2) = aux y table1