# HG changeset patch
# User paulson
# Date 982153606 -3600
# Node ID 2d92ab19747b529a6fb0d7cefb0b7481b4e5a923
# Parent  c3946a7cdee4fe7c0bb4c922f144b329be765dca
new function get_overloads

diff -r c3946a7cdee4 -r 2d92ab19747b src/Provers/blast.ML
--- 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) =