src/HOL/Tools/res_clause.ML
changeset 24322 dc7336b8c54c
parent 24310 af4af9993922
child 24937 340523598914
     1.1 --- a/src/HOL/Tools/res_clause.ML	Sat Aug 18 13:32:22 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Sat Aug 18 13:32:23 2007 +0200
     1.3 @@ -43,7 +43,6 @@
     1.4    datatype type_literal = LTVar of string * string | LTFree of string * string
     1.5    val mk_typ_var_sort: typ -> typ_var * sort
     1.6    exception CLAUSE of string * term
     1.7 -  val init : theory -> unit
     1.8    val isMeta : string -> bool
     1.9    val add_typs_aux : (typ_var * string list) list -> type_literal list * type_literal list
    1.10    val get_tvar_strs: (typ_var * sort) list -> string list
    1.11 @@ -266,16 +265,6 @@
    1.12  exception CLAUSE of string * term;
    1.13  
    1.14  
    1.15 -(*Declarations of the current theory--to allow suppressing types.*)
    1.16 -val const_typargs = ref (Library.K [] : (string*typ -> typ list));
    1.17 -
    1.18 -fun num_typargs(s,T) = length (!const_typargs (s,T));
    1.19 -
    1.20 -(*Initialize the type suppression mechanism with the current theory before
    1.21 -    producing any clauses!*)
    1.22 -fun init thy = (const_typargs := Sign.const_typargs thy);
    1.23 -
    1.24 -
    1.25  (*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and
    1.26    TVars it contains.*)
    1.27  fun type_of (Type (a, Ts)) =