diff -r 0605d90be6fc -r dfc7a46c2900 src/HOL/Nitpick_Examples/Mono_Nits.thy --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Wed Apr 02 20:41:44 2014 +0200 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Apr 03 10:51:20 2014 +0200 @@ -143,15 +143,6 @@ val preproc_timeout = seconds 5.0 val mono_timeout = seconds 1.0 -fun all_unconcealed_theorems_of thy = - let val facts = Global_Theory.facts_of thy in - Facts.fold_static - (fn (name, ths) => - if Facts.is_concealed facts name then I - else append (map (`(Thm.get_name_hint)) ths)) - facts [] - end - fun is_forbidden_theorem name = length (Long_Name.explode name) <> 2 orelse String.isPrefix "type_definition" (List.last (Long_Name.explode name)) orelse @@ -163,7 +154,7 @@ filter (fn (name, th) => not (is_forbidden_theorem name) andalso (theory_of_thm th, thy) |> pairself Context.theory_name |> op =) - (all_unconcealed_theorems_of thy) + (Global_Theory.all_thms_of thy true) fun check_formulas tsp = let