Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix non-exhaustive pattern match in find_theorems
authornoschinl
Wed, 23 Feb 2011 17:40:28 +0100
changeset 41835 9712fae15200
parent 41834 2f8f2685e0c0
child 41836 c9d788ff7940
fix non-exhaustive pattern match in find_theorems
src/Pure/Tools/find_theorems.ML file | annotate | diff | comparison | revisions 
--- 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"
isabelle