changeset 60638 | 16d80e5ef2dc |
parent 59582 | 0fbed69ff081 |
child 61076 | bdc1e2f0a86a |
--- 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 =