Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/predicate_compile.ML
changeset 33317 b4534348b8fd
parent 33042 ddf1f03a9ad9 
--- a/src/HOL/ex/predicate_compile.ML	Thu Oct 29 16:59:12 2009 +0100
+++ b/src/HOL/ex/predicate_compile.ML	Thu Oct 29 17:58:26 2009 +0100
@@ -999,7 +999,7 @@
 
 fun check_modes_pred with_generator thy param_vs preds modes gen_modes (p, ms) =
   let val SOME rs = AList.lookup (op =) preds p
-  in (p, List.filter (fn m => case find_index
+  in (p, filter (fn m => case find_index
     (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
       ~1 => true
     | i => (tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
isabelle