--- 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);