--- a/thys/Recursive.thy	Wed Dec 19 16:47:10 2018 +0100
+++ b/thys/Recursive.thy	Fri Dec 21 12:31:36 2018 +0100
@@ -2794,5 +2794,7 @@
     using wf_tm_from_abacus[of "tm_of (a [+] dummy_abc b)" "(a [+] dummy_abc b)" b]
     by simp
 qed
- 
+
+unused_thms
+
 end
\ No newline at end of file