src/FOL/fologic.ML

--- a/src/FOL/fologic.ML	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/FOL/fologic.ML	Mon Dec 20 16:44:33 2010 +0100
@@ -50,29 +50,29 @@
 (* Logical constants *)
 
 val not = Const (@{const_name Not}, oT --> oT);
-val conj = Const(@{const_name "op &"}, [oT,oT]--->oT);
-val disj = Const(@{const_name "op |"}, [oT,oT]--->oT);
-val imp = Const(@{const_name "op -->"}, [oT,oT]--->oT)
-val iff = Const(@{const_name "op <->"}, [oT,oT]--->oT);
+val conj = Const(@{const_name conj}, [oT,oT]--->oT);
+val disj = Const(@{const_name disj}, [oT,oT]--->oT);
+val imp = Const(@{const_name imp}, [oT,oT]--->oT)
+val iff = Const(@{const_name iff}, [oT,oT]--->oT);
 
 fun mk_conj (t1, t2) = conj $ t1 $ t2
 and mk_disj (t1, t2) = disj $ t1 $ t2
 and mk_imp (t1, t2) = imp $ t1 $ t2
 and mk_iff (t1, t2) = iff $ t1 $ t2;
 
-fun dest_imp (Const(@{const_name "op -->"},_) $ A $ B) = (A, B)
+fun dest_imp (Const(@{const_name imp},_) $ A $ B) = (A, B)
   | dest_imp  t = raise TERM ("dest_imp", [t]);
 
-fun dest_conj (Const (@{const_name "op &"}, _) $ t $ t') = t :: dest_conj t'
+fun dest_conj (Const (@{const_name conj}, _) $ t $ t') = t :: dest_conj t'
   | dest_conj t = [t];
 
-fun dest_iff (Const(@{const_name "op <->"},_) $ A $ B) = (A, B)
+fun dest_iff (Const(@{const_name iff},_) $ A $ B) = (A, B)
   | dest_iff  t = raise TERM ("dest_iff", [t]);
 
-fun eq_const T = Const (@{const_name "op ="}, [T, T] ---> oT);
+fun eq_const T = Const (@{const_name eq}, [T, T] ---> oT);
 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
 
-fun dest_eq (Const (@{const_name "op ="}, _) $ lhs $ rhs) = (lhs, rhs)
+fun dest_eq (Const (@{const_name eq}, _) $ lhs $ rhs) = (lhs, rhs)
   | dest_eq t = raise TERM ("dest_eq", [t])
 
 fun all_const T = Const (@{const_name All}, [T --> oT] ---> oT);