--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Aug 27 10:56:46 2010 +0200
@@ -405,7 +405,7 @@
(* general syntactic functions *)
(*Like dest_conj, but flattens conjunctions however nested*)
-fun conjuncts_aux (Const (@{const_name "op &"}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
+fun conjuncts_aux (Const (@{const_name HOL.conj}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
| conjuncts_aux t conjs = t::conjs;
fun conjuncts t = conjuncts_aux t [];