# HG changeset patch
# User blanchet
# Date 1269266827 -3600
# Node ID 02595d4a3a7c48eaf110b498d3bea8dc79c0919f
# Parent  5ed2e9a545ac47046e9e45d084b791271806623d
detect OFCLASS() axioms in Nitpick;
this is necessary now that "Thy.all_axioms_of" returns such axiom (starting with change 46cfc4b8112e)

diff -r 5ed2e9a545ac -r 02595d4a3a7c src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 22 13:48:15 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 22 15:07:07 2010 +0100
@@ -1263,6 +1263,10 @@
          $ Const _ $ _)) =
     boring <> is_funky_typedef_name thy s andalso is_typedef thy s
   | is_typedef_axiom _ _ _ = false
+(* term -> bool *)
+fun is_class_axiom t =
+  (t |> Logic.strip_horn |> swap |> op :: |> map Logic.dest_of_class; true)
+  handle TERM _ => false
 
 (* Distinguishes between (1) constant definition axioms, (2) type arity and
    typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
@@ -1306,7 +1310,9 @@
   let
     (* theory list -> term list *)
     val axioms_of_thys =
-      maps Thm.axioms_of #> map (apsnd (subst_atomic subst o prop_of))
+      maps Thm.axioms_of
+      #> map (apsnd (subst_atomic subst o prop_of))
+      #> filter_out (is_class_axiom o snd)
     val specs = Defs.all_specifications_of (Theory.defs_of thy)
     val def_names = specs |> maps snd |> map_filter #def
                     |> OrdList.make fast_string_ord