--- a/src/HOL/Set.ML Thu Nov 20 10:50:51 1997 +0100
+++ b/src/HOL/Set.ML Thu Nov 20 10:54:04 1997 +0100
@@ -117,12 +117,12 @@
by (REPEAT (ares_tac (prems @ [ballI]) 1));
qed "subsetI";
-Blast.overload ("op <=", domain_type); (*The <= relation is overloaded*)
+Blast.overloaded ("op <=", domain_type); (*The <= relation is overloaded*)
(*While (:) is not, its type must be kept
for overloading of = to work.*)
-Blast.overload ("op :", domain_type);
-seq (fn a => Blast.overload (a, HOLogic.dest_setT o domain_type))
+Blast.overloaded ("op :", domain_type);
+seq (fn a => Blast.overloaded (a, HOLogic.dest_setT o domain_type))
["Ball", "Bex"];
(*need UNION, INTER also?*)
--- a/src/HOL/cladata.ML Thu Nov 20 10:50:51 1997 +0100
+++ b/src/HOL/cladata.ML Thu Nov 20 10:54:04 1997 +0100
@@ -78,7 +78,7 @@
end;
structure Blast = BlastFun(Blast_Data);
-Blast.overload ("op =", domain_type); (*overloading of equality as iff*)
+Blast.overloaded ("op =", domain_type); (*overloading of equality as iff*)
val Blast_tac = Blast.Blast_tac
and blast_tac = Blast.blast_tac;
--- a/src/Provers/blast.ML Thu Nov 20 10:50:51 1997 +0100
+++ b/src/Provers/blast.ML Thu Nov 20 10:54:04 1997 +0100
@@ -88,7 +88,7 @@
val depth_tac : claset -> int -> int -> tactic
val blast_tac : claset -> int -> tactic
val Blast_tac : int -> tactic
- val overload : string * (Term.typ -> Term.typ) -> unit
+ val overloaded : string * (Term.typ -> Term.typ) -> unit
(*debugging tools*)
val trace : bool ref
val fullTrace : branch list list ref
@@ -186,7 +186,7 @@
val overloads = ref ([]: (string * (Term.typ -> Term.typ)) list)
in
-fun overload arg = (overloads := arg :: (!overloads));
+fun overloaded arg = (overloads := arg :: (!overloads));
(*Convert a possibly overloaded Term.Const to a Blast.Const or Blast.TConst,
converting its type to a Blast.term in the latter case.*)