# HG changeset patch
# User boehmes
# Date 1251981064 -7200
# Node ID 7a06bf89c038b6d2af95b89527606d7251b7ec08
# Parent  14efbc20b70873c8f74c2a78793ec9c25b047e72
replaced backlist by whitelist

diff -r 14efbc20b708 -r 7a06bf89c038 src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Sep 03 14:05:13 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Sep 03 14:31:04 2009 +0200
@@ -112,12 +112,12 @@
 
 end
 
-val blacklist = ["disable_pr", "enable_pr", "done", ".", "using", "txt"]
+val whitelist = ["apply", "by", "proof"]
 
 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 =) blacklist (Toplevel.name_of tr))
+     member (op =) whitelist (Toplevel.name_of tr)
   then basic_hook tr (Toplevel.proof_of pre) (SOME post)
   else ()   (* FIXME: add theory_hook here *)