# HG changeset patch
# User wenzelm
# Date 1394881158 -3600
# Node ID 300f613060b0174a6c047f77ef7bbfef8515db04
# Parent  d348378ddf47969c285479c62aaacf42020a306a
tuned signature;
eliminated clones;

diff -r d348378ddf47 -r 300f613060b0 src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Sat Mar 15 11:57:55 2014 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Sat Mar 15 11:59:18 2014 +0100
@@ -180,7 +180,7 @@
 
 fun theorems_in_proof_term thm =
   let
-    val all_thms = Global_Theory.all_thms_of (Thm.theory_of_thm thm)
+    val all_thms = Global_Theory.all_thms_of (Thm.theory_of_thm thm) true
     fun collect (s, _, _) = if s <> "" then insert (op =) s else I
     fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE
     fun resolve_thms names = map_filter (member_of names) all_thms
diff -r d348378ddf47 -r 300f613060b0 src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Sat Mar 15 11:57:55 2014 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Sat Mar 15 11:59:18 2014 +0100
@@ -13,23 +13,11 @@
   val mutate_sign : term -> theory -> (string * string) list -> int -> term list 
   val mutate_mix : term -> theory -> string list -> 
    (string * string) list -> int -> term list
-
-  val all_unconcealed_thms_of : theory -> (string * thm) list
 end;
 
 structure Mutabelle : MUTABELLE = 
 struct
 
-fun all_unconcealed_thms_of thy =
-  let
-    val facts = Global_Theory.facts_of thy
-  in
-    Facts.fold_static
-      (fn (s, ths) =>
-        if Facts.is_concealed facts s then I else append (map (`(Thm.get_name_hint)) ths))
-      facts []
-  end;
-
 fun consts_of thy =
  let
    val {const_space, constants, ...} = Consts.dest (Sign.consts_of thy)
diff -r d348378ddf47 -r 300f613060b0 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Mar 15 11:57:55 2014 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Mar 15 11:59:18 2014 +0100
@@ -336,7 +336,7 @@
   filter
     (fn th => (all orelse Context.theory_name (theory_of_thm th) = Context.theory_name thy)
       (* andalso is_executable_thm thy th *))
-    (map snd (filter_out is_forbidden_theorem (Mutabelle.all_unconcealed_thms_of thy)))
+    (map snd (filter_out is_forbidden_theorem (Global_Theory.all_thms_of thy false)))
 
 fun elapsed_time description e =
   let val ({elapsed, ...}, result) = Timing.timing e ()
diff -r d348378ddf47 -r 300f613060b0 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Mar 15 11:57:55 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Mar 15 11:59:18 2014 +0100
@@ -2000,7 +2000,7 @@
 fun ground_theorem_table thy =
   fold ((fn @{const Trueprop} $ t1 =>
             is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
-          | _ => I) o prop_of o snd) (Global_Theory.all_thms_of thy) Inttab.empty
+          | _ => I) o prop_of o snd) (Global_Theory.all_thms_of thy true) Inttab.empty
 
 fun ersatz_table ctxt =
  #ersatz_table (Data.get (Context.Proof ctxt))
diff -r d348378ddf47 -r 300f613060b0 src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Sat Mar 15 11:57:55 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Sat Mar 15 11:59:18 2014 +0100
@@ -13,17 +13,7 @@
 structure Find_Unused_Assms : FIND_UNUSED_ASSMS =
 struct
 
-fun all_unconcealed_thms_of thy =
-  let
-    val facts = Global_Theory.facts_of thy
-  in
-    Facts.fold_static
-      (fn (s, ths) =>
-        if Facts.is_concealed facts s then I else append (map (`(Thm.get_name_hint)) ths))
-      facts []
-  end
-
-fun thms_of thy thy_name = all_unconcealed_thms_of thy
+fun thms_of thy thy_name = Global_Theory.all_thms_of thy false
   |> filter (fn (_, th) => Context.theory_name (theory_of_thm th) = thy_name)
 
 fun do_while P f s list =
diff -r d348378ddf47 -r 300f613060b0 src/Pure/Proof/proof_checker.ML
--- a/src/Pure/Proof/proof_checker.ML	Sat Mar 15 11:57:55 2014 +0100
+++ b/src/Pure/Proof/proof_checker.ML	Sat Mar 15 11:59:18 2014 +0100
@@ -16,7 +16,7 @@
 (***** construct a theorem out of a proof term *****)
 
 fun lookup_thm thy =
-  let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty in
+  let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy true) Symtab.empty in
     fn s =>
       (case Symtab.lookup tab s of
         NONE => error ("Unknown theorem " ^ quote s)
diff -r d348378ddf47 -r 300f613060b0 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Sat Mar 15 11:57:55 2014 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Sat Mar 15 11:59:18 2014 +0100
@@ -87,7 +87,7 @@
 
 fun proof_of_term thy ty =
   let
-    val thms = Global_Theory.all_thms_of thy;
+    val thms = Global_Theory.all_thms_of thy true;
     val axms = Theory.all_axioms_of thy;
 
     fun mk_term t = (if ty then I else map_types (K dummyT))
@@ -187,7 +187,7 @@
 
 fun cterm_of_proof thy prf =
   let
-    val thm_names = map fst (Global_Theory.all_thms_of thy);
+    val thm_names = map fst (Global_Theory.all_thms_of thy true);
     val axm_names = map fst (Theory.all_axioms_of thy);
     val thy' = thy
       |> add_proof_syntax
@@ -199,7 +199,7 @@
 
 fun read_term thy topsort =
   let
-    val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy));
+    val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy true));
     val axm_names = map fst (Theory.all_axioms_of thy);
     val ctxt = thy
       |> add_proof_syntax
diff -r d348378ddf47 -r 300f613060b0 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Sat Mar 15 11:57:55 2014 +0100
+++ b/src/Pure/global_theory.ML	Sat Mar 15 11:59:18 2014 +0100
@@ -13,7 +13,7 @@
   val hide_fact: bool -> string -> theory -> theory
   val get_thms: theory -> xstring -> thm list
   val get_thm: theory -> xstring -> thm
-  val all_thms_of: theory -> (string * thm) list
+  val all_thms_of: theory -> bool -> (string * thm) list
   val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
   val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list
   val burrow_facts: ('a list -> 'b list) ->
@@ -71,8 +71,13 @@
 fun get_thm thy xname =
   Facts.the_single (xname, Position.none) (get_thms thy xname);
 
-fun all_thms_of thy =
-  Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) [];
+fun all_thms_of thy verbose =
+  let
+    val facts = facts_of thy;
+    fun add (name, ths) =
+      if not verbose andalso Facts.is_concealed facts name then I
+      else append (map (`(Thm.get_name_hint)) ths);
+  in Facts.fold_static add facts [] end;