src/HOL/Nitpick_Examples/Mono_Nits.thy

--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Fri Jul 03 14:32:55 2015 +0200
@@ -153,7 +153,7 @@
 fun theorems_of thy =
   filter (fn (name, th) =>
              not (is_forbidden_theorem name) andalso
-             (Thm.theory_of_thm th, thy) |> apply2 Context.theory_name |> op =)
+             Thm.theory_name_of_thm th = Context.theory_name thy)
          (Global_Theory.all_thms_of thy true)
 
 fun check_formulas tsp =