removed clone (cf. 300f613060b0)
authorblanchet
Thu, 03 Apr 2014 10:51:20 +0200
changeset 56374 dfc7a46c2900
parent 56373 0605d90be6fc
child 56375 32e0da92c786
removed clone (cf. 300f613060b0)
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