reset clause counter
authorpaulson
Tue, 04 Oct 2005 09:58:38 +0200
changeset 17745 38b4d8bf2627
parent 17744 3007c82f17ca
child 17746 af59c748371d
reset clause counter
src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Tue Oct 04 09:58:17 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML	Tue Oct 04 09:58:38 2005 +0200
@@ -275,7 +275,7 @@
 
 (*Initialize the type suppression mechanism with the current theory before
     producing any clauses!*)
-fun init thy = (curr_defs := Theory.defs_of thy);
+fun init thy = (id_ref := 0; curr_defs := Theory.defs_of thy);
 
 fun no_types_needed s = Defs.monomorphic (!curr_defs) s;