--- a/src/HOL/ex/SVC_Oracle.thy Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Thu Aug 26 20:51:17 2010 +0200
@@ -90,7 +90,7 @@
(*abstraction of a formula*)
and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
| fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
- | fm ((c as Const(@{const_name "op -->"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+ | fm ((c as Const(@{const_name HOL.implies}, _)) $ p $ q) = c $ (fm p) $ (fm q)
| fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
| fm ((c as Const(@{const_name True}, _))) = c
| fm ((c as Const(@{const_name False}, _))) = c