--- 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
--- 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)
--- 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 ()
--- 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))
--- 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 =
--- 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)
--- 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
--- 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;