# HG changeset patch
# User wenzelm
# Date 1130414080 -7200
# Node ID e6e5b28740ec432cd8a27388631067f400c1c99c
# Parent  4379d46c8e136d05a2fda68749865c883db0b4a1
replaced Defs.monomorphic by Sign.monomorphic;

diff -r 4379d46c8e13 -r e6e5b28740ec src/HOL/Tools/res_clause.ML
--- 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
diff -r 4379d46c8e13 -r e6e5b28740ec src/Provers/blast.ML
--- 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.