# HG changeset patch
# User wenzelm
# Date 1130939213 -3600
# Node ID f453c2cd44081dc79924a53aadfb4e6f9db44ca4
# Parent  ad97e231bf8aecf1578f39c82a44a6a0a3179500
fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;

diff -r ad97e231bf8a -r f453c2cd4408 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Wed Nov 02 14:46:51 2005 +0100
+++ b/src/Provers/blast.ML	Wed Nov 02 14:46:53 2005 +0100
@@ -178,17 +178,16 @@
 		 | SOME v => v)
 
 (*refer to the theory in which blast is initialized*)
-val monomorphic = ref (fn (_: string) => false);
+val typargs = ref (fn (_: string) => fn (T: typ) => [T]);
 
 (*Convert a Term.Const to a Blast.Const or Blast.TConst,
-  converting its type to a Blast.term in the latter case.
-  For efficiency, Const is used for FOL and for the logical constants.
-  We can't use it for all non-overloaded operators because some preservation
-  of type information is necessary to prevent PROOF FAILED elsewhere.*)
-fun fromConst alist (a,T) = 
-  if not Data.is_hol orelse a mem_string ["All","Ex","all"] orelse
-    ! monomorphic a then Const a
-  else TConst(a, fromType alist T);
+  converting its type to a Blast.term in the latter case.*)
+fun fromConst alist (a as "all", _) = Const a
+  | fromConst alist (a, T) =
+      (case ! typargs a T of
+        [] => Const a
+      | [T] => TConst (a, fromType alist T)
+      | Ts => TConst (a, list_comb (Const "*typargs*", map (fromType alist) Ts)));
 
 
 (*Tests whether 2 terms are alpha-convertible; chases instantiations*)
@@ -1242,7 +1241,7 @@
 
 fun initialize thy = 
     (fullTrace:=[];  trail := [];  ntrail := 0;
-     nclosed := 0;  ntried := 1;  monomorphic := Sign.monomorphic thy);
+     nclosed := 0;  ntried := 1;  typargs := Sign.const_typargs thy);
 
 
 (*Tactic using tableau engine and proof reconstruction.