diff -r 970508a5119f -r eba0175d4cd1 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Aug 27 09:34:06 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Aug 27 09:43:52 2010 +0200
@@ -664,10 +664,10 @@
 
 (* FIXME: large copy of Predicate_Compile_Quickcheck - refactor out commons *)
 
-fun strip_imp_prems (Const(@{const_name "op -->"}, _) $ A $ B) = A :: strip_imp_prems B
+fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
   | strip_imp_prems _ = [];
 
-fun strip_imp_concl (Const(@{const_name "op -->"}, _) $ A $ B) = strip_imp_concl B
+fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
   | strip_imp_concl A = A : term;
 
 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);