--- a/src/HOL/ex/SVC_Oracle.thy Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Thu Aug 19 16:08:59 2010 +0200
@@ -91,15 +91,15 @@
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 "Not"}, _)) $ p) = c $ (fm p)
- | fm ((c as Const(@{const_name "True"}, _))) = c
- | fm ((c as Const(@{const_name "False"}, _))) = c
+ | 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
| fm (t as Const(@{const_name "op ="}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm t = replace t
(*entry point, and abstraction of a meta-formula*)
- fun mt ((c as Const(@{const_name "Trueprop"}, _)) $ p) = c $ (fm p)
+ fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p)
| mt ((c as Const("==>", _)) $ p $ q) = c $ (mt p) $ (mt q)
| mt t = fm t (*it might be a formula*)
in (list_all (params, mt body), !pairs) end;