--- a/src/Provers/blast.ML Wed Feb 14 13:19:14 2001 +0100
+++ b/src/Provers/blast.ML Wed Feb 14 13:26:46 2001 +0100
@@ -91,6 +91,7 @@
val blast_tac : claset -> int -> tactic
val Blast_tac : int -> tactic
val overloaded : string * (Term.typ -> Term.typ) -> unit
+ val get_overloads : unit -> (string * (Term.typ -> Term.typ)) list
val setup : (theory -> theory) list
(*debugging tools*)
val stats : bool ref
@@ -194,6 +195,8 @@
fun overloaded arg = (overloads := arg :: (!overloads));
+fun get_overloads() = !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.*)
fun fromConst alist (a,T) =