src/HOL/cladata.ML
changeset 4240 8ba60a4cd380
parent 4223 f60e3d2c81d3
child 4305 03d7de40ee4f
     1.1 --- a/src/HOL/cladata.ML	Thu Nov 20 10:50:51 1997 +0100
     1.2 +++ b/src/HOL/cladata.ML	Thu Nov 20 10:54:04 1997 +0100
     1.3 @@ -78,7 +78,7 @@
     1.4    end;
     1.5  
     1.6  structure Blast = BlastFun(Blast_Data);
     1.7 -Blast.overload ("op =", domain_type);	(*overloading of equality as iff*)
     1.8 +Blast.overloaded ("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;