fix non-exhaustive pattern match in find_theorems
authornoschinl
Wed Feb 23 17:40:28 2011 +0100 (2011-02-23)
changeset 418359712fae15200
parent 41834 2f8f2685e0c0
child 41836 c9d788ff7940
fix non-exhaustive pattern match in find_theorems
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Wed Feb 23 11:42:01 2011 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed Feb 23 17:40:28 2011 +0100
     1.3 @@ -263,6 +263,7 @@
     1.4  
     1.5  fun filter_crit _ _ (Name name) = apfst (filter_name name)
     1.6    | filter_crit _ NONE Intro = err_no_goal "intro"
     1.7 +  | filter_crit _ NONE IntroIff = err_no_goal "introiff"
     1.8    | filter_crit _ NONE Elim = err_no_goal "elim"
     1.9    | filter_crit _ NONE Dest = err_no_goal "dest"
    1.10    | filter_crit _ NONE Solves = err_no_goal "solves"