changeset 13105 | 3d1e7a199bdc |
parent 13038 | e968745986f1 |
child 14162 | f05f299512e9 |
1.1 --- a/src/HOL/Tools/inductive_codegen.ML Tue May 07 14:24:30 2002 +0200 1.2 +++ b/src/HOL/Tools/inductive_codegen.ML Tue May 07 14:26:32 2002 +0200 1.3 @@ -26,7 +26,7 @@ 1.4 val empty = Symtab.empty; 1.5 val copy = I; 1.6 val prep_ext = I; 1.7 - val merge = Symtab.merge_multi eq_thm; 1.8 + val merge = Symtab.merge_multi Drule.eq_thm_prop; 1.9 fun print _ _ = (); 1.10 end; 1.11