--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML Mon Aug 31 17:32:29 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML Mon Aug 31 19:28:37 2009 +0200
@@ -116,10 +116,12 @@
end
+val blacklist = ["disable_pr", "enable_pr", "done", "."]
+
fun step_hook tr pre post =
(* FIXME: might require wrapping into "interruptible" *)
if can (Proof.assert_backward o Toplevel.proof_of) pre andalso
- not (member (op =) ["disable_pr", "enable_pr"] (Toplevel.name_of tr))
+ not (member (op =) blacklist (Toplevel.name_of tr))
then basic_hook tr (Toplevel.proof_of pre) (SOME post)
else () (* FIXME: add theory_hook here *)