diff -r 43e4d63c93df -r 3e3480647439 TODO.md
--- a/TODO.md	Tue Aug 17 21:57:40 2021 +0200
+++ b/TODO.md	Tue Aug 17 22:39:48 2021 +0200
@@ -10,12 +10,6 @@
     76a77
     >       "src/Tools/isac/etc" -> Path.explode("isabelle.isac"),
 
-* MW: exception TYPE raised by Skip_Proof.make_thm, see
-    https://hg.risc.uni-linz.ac.at/wneuper/isa/file/a14022b99b92/src/Tools/isac/ProgLang/evaluate.sml#l210
-
-* MW: error with \<^rule_thm>\<open>filterVar.simps(1)\<close>
-    https://hg.risc.uni-linz.ac.at/wneuper/isa/diff/4f5f29fd0af9/src/Tools/isac/Knowledge/DiffApp.thy#l1.34
-
 * Eliminate Thy_Info.get_theory eventually: should take theory from ancestory
   within current context.
     cf. e587c45cae0f note in Build_Thydata.thy