--- a/src/HOL/ex/SVC_Oracle.thy Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Fri Aug 27 10:56:46 2010 +0200
@@ -88,8 +88,8 @@
else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
else replace (c $ x $ y) (*non-numeric comparison*)
(*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)
+ and fm ((c as Const(@{const_name HOL.conj}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+ | fm ((c as Const(@{const_name HOL.disj}, _)) $ 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