# HG changeset patch
# User blanchet
# Date 1266845770 -3600
# Node ID 7ae51d5ea05de636ca33b41ccae031d15ec4e6b3
# Parent  54ab4921f826386eb127226674dac672e61028e8
filter out trivial definitions in Nitpick (e.g. "Topology.topo" from AFP)

diff -r 54ab4921f826 -r 7ae51d5ea05d src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 22 11:57:33 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 22 14:36:10 2010 +0100
@@ -1143,6 +1143,8 @@
 fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute})
 
 (* term -> bool *)
+val is_trivial_definition =
+  the_default false o try (op aconv o Logic.dest_equals)
 val is_plain_definition =
   let
     (* term -> bool *)
@@ -1180,7 +1182,9 @@
     val defs =
       (thy |> PureThy.all_thms_of
            |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd)
-           |> map (prop_of o snd) |> filter is_plain_definition) @
+           |> map (prop_of o snd)
+           |> filter_out is_trivial_definition
+           |> filter is_plain_definition) @
       user_defs @ built_in_defs
   in (defs, built_in_nondefs, user_nondefs) end