diff -r 3007c82f17ca -r 38b4d8bf2627 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;