--- a/src/HOL/Tools/res_clause.ML Thu Oct 27 13:54:38 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML Thu Oct 27 13:54:40 2005 +0200
@@ -272,14 +272,13 @@
-(*Definitions of the current theory--to allow suppressing types.*)
-val curr_defs = ref Defs.empty;
+(*Declarations of the current theory--to allow suppressing types.*)
+val monomorphic = ref (fn (_: string) => false);
+fun no_types_needed s = ! monomorphic s;
(*Initialize the type suppression mechanism with the current theory before
producing any clauses!*)
-fun init thy = (curr_defs := Theory.defs_of thy);
-
-fun no_types_needed s = Defs.monomorphic (!curr_defs) s;
+fun init thy = (monomorphic := Sign.monomorphic thy);
(*Flatten a type to a string while accumulating sort constraints on the TFress and
--- 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.