# HG changeset patch
# User nipkow
# Date 1251886817 -7200
# Node ID 071e4ae8314942caccf0f6f6285c7065d90ab00f
# Parent  1521d879daf4ab909c51d2d68720d60e6856f655
added "using" to blacklist

diff -r 1521d879daf4 -r 071e4ae83149 src/HOL/Tools/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML	Wed Sep 02 10:54:52 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML	Wed Sep 02 12:20:17 2009 +0200
@@ -112,7 +112,7 @@
 
 end
 
-val blacklist = ["disable_pr", "enable_pr", "done", ".", "txt"]
+val blacklist = ["disable_pr", "enable_pr", "done", ".", "using", "txt"]
 
 fun step_hook tr pre post =
  (* FIXME: might require wrapping into "interruptible" *)