src/Provers/blast.ML
changeset 4240 8ba60a4cd380
parent 4233 85d004a96b98
child 4271 3a82492e70c5
     1.1 --- a/src/Provers/blast.ML	Thu Nov 20 10:50:51 1997 +0100
     1.2 +++ b/src/Provers/blast.ML	Thu Nov 20 10:54:04 1997 +0100
     1.3 @@ -88,7 +88,7 @@
     1.4    val depth_tac 	: claset -> int -> int -> tactic
     1.5    val blast_tac 	: claset -> int -> tactic
     1.6    val Blast_tac 	: int -> tactic
     1.7 -  val overload 	: string * (Term.typ -> Term.typ) -> unit
     1.8 +  val overloaded 	: string * (Term.typ -> Term.typ) -> unit
     1.9    (*debugging tools*)
    1.10    val trace	        : bool ref
    1.11    val fullTrace	        : branch list list ref
    1.12 @@ -186,7 +186,7 @@
    1.13  val overloads = ref ([]: (string * (Term.typ -> Term.typ)) list)
    1.14  in
    1.15  
    1.16 -fun overload arg = (overloads := arg :: (!overloads));
    1.17 +fun overloaded arg = (overloads := arg :: (!overloads));
    1.18  
    1.19  (*Convert a possibly overloaded Term.Const to a Blast.Const or Blast.TConst,
    1.20    converting its type to a Blast.term in the latter case.*)