diff -r ee6e3597bb4d -r 803c94363ccc src/CCL/Term.thy
--- a/src/CCL/Term.thy	Mon Oct 09 02:20:09 2006 +0200
+++ b/src/CCL/Term.thy	Mon Oct 09 02:20:10 2006 +0200
@@ -309,17 +309,16 @@
 bind_thms ("term_porews", term_porews);
 *}
 
-
 subsection {* Rewriting and Proving *}
 
-lemmas term_rews = termBs term_injs term_dstncts ccl_porews term_porews
-
 ML {*
   bind_thms ("term_injDs", XH_to_Ds term_injs);
 *}
 
+lemmas term_rews = termBs term_injs term_dstncts ccl_porews term_porews
+
 lemmas [simp] = term_rews
-  and [elim!] = term_dstncts [THEN notE]
-  and [dest!] = term_injDs
+lemmas [elim!] = term_dstncts [THEN notE]
+lemmas [dest!] = term_injDs
 
 end