--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Mar 26 14:13:03 2019 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Mar 26 14:23:18 2019 +0100
@@ -1354,7 +1354,7 @@
fun all_nondefs_of ctxt subst =
ctxt |> Spec_Rules.get
- |> filter (curry (op =) Spec_Rules.Unknown o fst)
+ |> filter (Spec_Rules.is_unknown o fst)
|> maps (snd o snd)
|> filter_out (is_built_in_theory o Thm.theory_id)
|> map (subst_atomic subst o Thm.prop_of)
@@ -1948,8 +1948,8 @@
def_table_for
(maps (map (unfold_mutually_inductive_preds thy def_tables o Thm.prop_of)
o snd o snd)
- (filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse
- cat = Spec_Rules.Co_Inductive) (Spec_Rules.get ctxt))) subst
+ (filter ((Spec_Rules.is_inductive orf Spec_Rules.is_co_inductive) o #1)
+ (Spec_Rules.get ctxt))) subst
end
fun ground_theorem_table thy =