--- a/src/HOL/Tools/hologic.ML Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Tools/hologic.ML Fri Aug 27 19:34:23 2010 +0200
@@ -49,7 +49,7 @@
val exists_const: typ -> term
val mk_exists: string * typ * term -> term
val choice_const: typ -> term
- val class_eq: string
+ val class_equal: string
val mk_binop: string -> term * term -> term
val mk_binrel: string -> term * term -> term
val dest_bin: string -> typ -> term -> term * term
@@ -251,7 +251,7 @@
fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);
-val class_eq = "HOL.eq";
+val class_equal = "HOL.equal";
(* binary operations and relations *)