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