# HG changeset patch
# User paulson
# Date 880019644 -3600
# Node ID 8ba60a4cd380ac9920c677324651249eb894a6e6
# Parent  8c98484ef66f56e89b6727df83b068f7bd8ed261
Renamed "overload" to "overloaded" for sml/nj compatibility

diff -r 8c98484ef66f -r 8ba60a4cd380 src/HOL/Set.ML
--- 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?*)
 
diff -r 8c98484ef66f -r 8ba60a4cd380 src/HOL/cladata.ML
--- 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;
diff -r 8c98484ef66f -r 8ba60a4cd380 src/Provers/blast.ML
--- 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.*)