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