diff -r 2d638e963357 -r 848be46708dc src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Aug 27 10:55:20 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Aug 27 10:56:46 2010 +0200 @@ -221,8 +221,8 @@ @{const_name HOL.implies}, @{const_name All}, @{const_name Ex}, - @{const_name "op &"}, - @{const_name "op |"}] + @{const_name HOL.conj}, + @{const_name HOL.disj}] fun special_cases (c, T) = member (op =) [ @{const_name Product_Type.Unity},