# HG changeset patch
# User noschinl
# Date 1298479228 -3600
# Node ID 9712fae15200a86e5e92c3df5b03f64cf108f793
# Parent  2f8f2685e0c08cc051bb0407f1030f9d1cfa43ae
fix non-exhaustive pattern match in find_theorems

diff -r 2f8f2685e0c0 -r 9712fae15200 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Wed Feb 23 11:42:01 2011 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Wed Feb 23 17:40:28 2011 +0100
@@ -263,6 +263,7 @@
 
 fun filter_crit _ _ (Name name) = apfst (filter_name name)
   | filter_crit _ NONE Intro = err_no_goal "intro"
+  | filter_crit _ NONE IntroIff = err_no_goal "introiff"
   | filter_crit _ NONE Elim = err_no_goal "elim"
   | filter_crit _ NONE Dest = err_no_goal "dest"
   | filter_crit _ NONE Solves = err_no_goal "solves"