--- a/src/Provers/blast.ML Thu Oct 27 13:54:38 2005 +0200
+++ b/src/Provers/blast.ML Thu Oct 27 13:54:40 2005 +0200
@@ -177,8 +177,8 @@
end
| SOME v => v)
-(*Definitions of the theory in which blast is initialized.*)
-val curr_defs = ref Defs.empty;
+(*refer to the theory in which blast is initialized*)
+val monomorphic = ref (fn (_: string) => false);
(*Convert a Term.Const to a Blast.Const or Blast.TConst,
converting its type to a Blast.term in the latter case.
@@ -187,7 +187,7 @@
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
- Defs.monomorphic (!curr_defs) a then Const a
+ ! monomorphic a then Const a
else TConst(a, fromType alist T);
@@ -1242,7 +1242,7 @@
fun initialize thy =
(fullTrace:=[]; trail := []; ntrail := 0;
- nclosed := 0; ntried := 1; curr_defs := Theory.defs_of thy);
+ nclosed := 0; ntried := 1; monomorphic := Sign.monomorphic thy);
(*Tactic using tableau engine and proof reconstruction.