author | paulson |
Tue, 04 Oct 2005 09:58:38 +0200 | |
changeset 17745 | 38b4d8bf2627 |
parent 17744 | 3007c82f17ca |
child 17746 | af59c748371d |
--- 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;