--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Aug 26 20:51:17 2010 +0200
@@ -595,10 +595,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);