diff -r 2d638e963357 -r 848be46708dc src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Aug 27 10:56:46 2010 +0200
@@ -2954,8 +2954,8 @@
 fun powt rT = Const(@{const_name "power"}, [rT,@{typ "nat"}] ---> rT);
 val brT = [bT, bT] ---> bT;
 val nott = @{term "Not"};
-val conjt = @{term "op &"};
-val disjt = @{term "op |"};
+val conjt = @{term HOL.conj};
+val disjt = @{term HOL.disj};
 val impt = @{term HOL.implies};
 val ifft = @{term "op = :: bool => _"}
 fun llt rT = Const(@{const_name Orderings.less},rrT rT);
@@ -3018,8 +3018,8 @@
     Const(@{const_name True},_) => @{code T}
   | Const(@{const_name False},_) => @{code F}
   | Const(@{const_name Not},_)$p => @{code NOT} (fm_of_term m m' p)
-  | Const(@{const_name "op &"},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
-  | Const(@{const_name "op |"},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
+  | Const(@{const_name HOL.conj},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
+  | Const(@{const_name HOL.disj},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
   | Const(@{const_name HOL.implies},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
   | Const(@{const_name "op ="},ty)$p$q => 
        if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)