diff -r 7fbc4fc400d8 -r d721d21e6374 src/CCL/Term.thy
--- 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"]]);
 *}