src/HOL/cladata.ML
changeset 4059 59c1422c9da5
parent 3842 b55686a7b22c
child 4085 6e2d41a5ea43
     1.1 --- a/src/HOL/cladata.ML	Sat Nov 01 12:58:08 1997 +0100
     1.2 +++ b/src/HOL/cladata.ML	Sat Nov 01 12:59:06 1997 +0100
     1.3 @@ -93,7 +93,7 @@
     1.4    end;
     1.5  
     1.6  structure Blast = BlastFun(Blast_Data);
     1.7 -Blast.declConsts (["op ="], [iffI]);	(*overloading of equality as iff*)
     1.8 +Blast.overload ("op =", domain_type);	(*overloading of equality as iff*)
     1.9  
    1.10  val Blast_tac = Blast.Blast_tac
    1.11  and blast_tac = Blast.blast_tac;