src/HOL/Tools/res_clause.ML
changeset 17745 38b4d8bf2627
parent 17525 ae5bb6001afb
child 17764 fde495b9e24b
equal deleted inserted replaced
17744:3007c82f17ca 17745:38b4d8bf2627
   273 (*Definitions of the current theory--to allow suppressing types.*)
   273 (*Definitions of the current theory--to allow suppressing types.*)
   274 val curr_defs = ref Defs.empty;
   274 val curr_defs = ref Defs.empty;
   275 
   275 
   276 (*Initialize the type suppression mechanism with the current theory before
   276 (*Initialize the type suppression mechanism with the current theory before
   277     producing any clauses!*)
   277     producing any clauses!*)
   278 fun init thy = (curr_defs := Theory.defs_of thy);
   278 fun init thy = (id_ref := 0; curr_defs := Theory.defs_of thy);
   279 
   279 
   280 fun no_types_needed s = Defs.monomorphic (!curr_defs) s;
   280 fun no_types_needed s = Defs.monomorphic (!curr_defs) s;
   281     
   281     
   282 
   282 
   283 (*Flatten a type to a string while accumulating sort constraints on the TFress and
   283 (*Flatten a type to a string while accumulating sort constraints on the TFress and