src/HOL/Tools/hologic.ML
changeset 38857 97775f3e8722
parent 38795 848be46708dc
child 38864 4abe644fcea5
     1.1 --- a/src/HOL/Tools/hologic.ML	Fri Aug 27 15:36:02 2010 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Fri Aug 27 19:34:23 2010 +0200
     1.3 @@ -49,7 +49,7 @@
     1.4    val exists_const: typ -> term
     1.5    val mk_exists: string * typ * term -> term
     1.6    val choice_const: typ -> term
     1.7 -  val class_eq: string
     1.8 +  val class_equal: string
     1.9    val mk_binop: string -> term * term -> term
    1.10    val mk_binrel: string -> term * term -> term
    1.11    val dest_bin: string -> typ -> term -> term * term
    1.12 @@ -251,7 +251,7 @@
    1.13  
    1.14  fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);
    1.15  
    1.16 -val class_eq = "HOL.eq";
    1.17 +val class_equal = "HOL.equal";
    1.18  
    1.19  
    1.20  (* binary operations and relations *)