Renamed "overload" to "overloaded" for sml/nj compatibility
authorpaulson
Thu Nov 20 10:54:04 1997 +0100 (1997-11-20)
changeset 42408ba60a4cd380
parent 4239 8c98484ef66f
child 4241 3f3f87c6fe3b
Renamed "overload" to "overloaded" for sml/nj compatibility
src/HOL/Set.ML
src/HOL/cladata.ML
src/Provers/blast.ML
     1.1 --- a/src/HOL/Set.ML	Thu Nov 20 10:50:51 1997 +0100
     1.2 +++ b/src/HOL/Set.ML	Thu Nov 20 10:54:04 1997 +0100
     1.3 @@ -117,12 +117,12 @@
     1.4  by (REPEAT (ares_tac (prems @ [ballI]) 1));
     1.5  qed "subsetI";
     1.6  
     1.7 -Blast.overload ("op <=", domain_type); (*The <= relation is overloaded*)
     1.8 +Blast.overloaded ("op <=", domain_type); (*The <= relation is overloaded*)
     1.9  
    1.10  (*While (:) is not, its type must be kept
    1.11    for overloading of = to work.*)
    1.12 -Blast.overload ("op :", domain_type);
    1.13 -seq (fn a => Blast.overload (a, HOLogic.dest_setT o domain_type))
    1.14 +Blast.overloaded ("op :", domain_type);
    1.15 +seq (fn a => Blast.overloaded (a, HOLogic.dest_setT o domain_type))
    1.16      ["Ball", "Bex"];
    1.17  (*need UNION, INTER also?*)
    1.18  
     2.1 --- a/src/HOL/cladata.ML	Thu Nov 20 10:50:51 1997 +0100
     2.2 +++ b/src/HOL/cladata.ML	Thu Nov 20 10:54:04 1997 +0100
     2.3 @@ -78,7 +78,7 @@
     2.4    end;
     2.5  
     2.6  structure Blast = BlastFun(Blast_Data);
     2.7 -Blast.overload ("op =", domain_type);	(*overloading of equality as iff*)
     2.8 +Blast.overloaded ("op =", domain_type);	(*overloading of equality as iff*)
     2.9  
    2.10  val Blast_tac = Blast.Blast_tac
    2.11  and blast_tac = Blast.blast_tac;
     3.1 --- a/src/Provers/blast.ML	Thu Nov 20 10:50:51 1997 +0100
     3.2 +++ b/src/Provers/blast.ML	Thu Nov 20 10:54:04 1997 +0100
     3.3 @@ -88,7 +88,7 @@
     3.4    val depth_tac 	: claset -> int -> int -> tactic
     3.5    val blast_tac 	: claset -> int -> tactic
     3.6    val Blast_tac 	: int -> tactic
     3.7 -  val overload 	: string * (Term.typ -> Term.typ) -> unit
     3.8 +  val overloaded 	: string * (Term.typ -> Term.typ) -> unit
     3.9    (*debugging tools*)
    3.10    val trace	        : bool ref
    3.11    val fullTrace	        : branch list list ref
    3.12 @@ -186,7 +186,7 @@
    3.13  val overloads = ref ([]: (string * (Term.typ -> Term.typ)) list)
    3.14  in
    3.15  
    3.16 -fun overload arg = (overloads := arg :: (!overloads));
    3.17 +fun overloaded arg = (overloads := arg :: (!overloads));
    3.18  
    3.19  (*Convert a possibly overloaded Term.Const to a Blast.Const or Blast.TConst,
    3.20    converting its type to a Blast.term in the latter case.*)