| changeset 51670 | d721d21e6374 |
| parent 49660 | de49d9b4d7bc |
| child 51717 | 9e7d1c139569 |
--- a/src/CCL/Term.thy Wed Apr 10 12:24:43 2013 +0200 +++ b/src/CCL/Term.thy Wed Apr 10 12:31:35 2013 +0200 @@ -287,7 +287,7 @@ ML {* bind_thms ("term_dstncts", - mkall_dstnct_thms @{theory} @{thms data_defs} (@{thms ccl_injs} @ @{thms term_injs}) + mkall_dstnct_thms @{context} @{thms data_defs} (@{thms ccl_injs} @ @{thms term_injs}) [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]); *}