--- 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.*)