src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 33701 9dd1079cec3a
parent 33699 f33b036ef318
child 33706 7017aee615d6
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Nov 15 19:45:05 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Nov 15 20:39:22 2009 +0100
@@ -1044,7 +1044,7 @@
     (* theory list -> term list *)
     val axioms_of_thys = maps Thm.axioms_of #> map (apsnd prop_of)
     val specs = Defs.all_specifications_of (Theory.defs_of thy)
-    val def_names = specs |> maps snd |> filter #is_def |> map #name
+    val def_names = specs |> maps snd |> map_filter #def
                     |> OrdList.make fast_string_ord
     val thys = thy :: Theory.ancestors_of thy
     val (built_in_thys, user_thys) = List.partition is_built_in_theory thys