--- a/src/HOL/Prolog/prolog.ML Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Prolog/prolog.ML Fri Aug 27 10:56:46 2010 +0200
@@ -11,12 +11,12 @@
fun isD t = case t of
Const(@{const_name Trueprop},_)$t => isD t
- | Const(@{const_name "op &"} ,_)$l$r => isD l andalso isD r
+ | Const(@{const_name HOL.conj} ,_)$l$r => isD l andalso isD r
| Const(@{const_name HOL.implies},_)$l$r => isG l andalso isD r
| Const( "==>",_)$l$r => isG l andalso isD r
| Const(@{const_name All},_)$Abs(s,_,t) => isD t
| Const("all",_)$Abs(s,_,t) => isD t
- | Const(@{const_name "op |"},_)$_$_ => false
+ | Const(@{const_name HOL.disj},_)$_$_ => false
| Const(@{const_name Ex} ,_)$_ => false
| Const(@{const_name Not},_)$_ => false
| Const(@{const_name True},_) => false
@@ -30,8 +30,8 @@
and
isG t = case t of
Const(@{const_name Trueprop},_)$t => isG t
- | Const(@{const_name "op &"} ,_)$l$r => isG l andalso isG r
- | Const(@{const_name "op |"} ,_)$l$r => isG l andalso isG r
+ | Const(@{const_name HOL.conj} ,_)$l$r => isG l andalso isG r
+ | Const(@{const_name HOL.disj} ,_)$l$r => isG l andalso isG r
| Const(@{const_name HOL.implies},_)$l$r => isD l andalso isG r
| Const( "==>",_)$l$r => isD l andalso isG r
| Const(@{const_name All},_)$Abs(_,_,t) => isG t
@@ -53,7 +53,7 @@
fun at thm = case concl_of thm of
_$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS
(read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
- | _$(Const(@{const_name "op &"},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
+ | _$(Const(@{const_name HOL.conj},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
| _$(Const(@{const_name HOL.implies},_)$_$_) => at(thm RS mp)
| _ => [thm]
in map zero_var_indexes (at thm) end;