# HG changeset patch
# User wenzelm
# Date 1187436743 -7200
# Node ID dc7336b8c54cc5b5932d30be5867752e152f3192
# Parent  e9d99744e40c61434b1d622481dd1a55f38d1b1e
removed dead code: const_typargs, num_typargs, init;

diff -r e9d99744e40c -r dc7336b8c54c src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Sat Aug 18 13:32:22 2007 +0200
+++ b/src/HOL/Tools/res_clause.ML	Sat Aug 18 13:32:23 2007 +0200
@@ -43,7 +43,6 @@
   datatype type_literal = LTVar of string * string | LTFree of string * string
   val mk_typ_var_sort: typ -> typ_var * sort
   exception CLAUSE of string * term
-  val init : theory -> unit
   val isMeta : string -> bool
   val add_typs_aux : (typ_var * string list) list -> type_literal list * type_literal list
   val get_tvar_strs: (typ_var * sort) list -> string list
@@ -266,16 +265,6 @@
 exception CLAUSE of string * term;
 
 
-(*Declarations of the current theory--to allow suppressing types.*)
-val const_typargs = ref (Library.K [] : (string*typ -> typ list));
-
-fun num_typargs(s,T) = length (!const_typargs (s,T));
-
-(*Initialize the type suppression mechanism with the current theory before
-    producing any clauses!*)
-fun init thy = (const_typargs := Sign.const_typargs thy);
-
-
 (*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and
   TVars it contains.*)
 fun type_of (Type (a, Ts)) =