tuned signature;
authorwenzelm
Sat Mar 15 11:59:18 2014 +0100 (2014-03-15)
changeset 56161300f613060b0
parent 56160 d348378ddf47
child 56162 ea6303e2261b
tuned signature;
eliminated clones;
src/HOL/Mirabelle/Tools/mirabelle.ML
src/HOL/Mutabelle/mutabelle.ML
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Quickcheck/find_unused_assms.ML
src/Pure/Proof/proof_checker.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/global_theory.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Sat Mar 15 11:57:55 2014 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Sat Mar 15 11:59:18 2014 +0100
     1.3 @@ -180,7 +180,7 @@
     1.4  
     1.5  fun theorems_in_proof_term thm =
     1.6    let
     1.7 -    val all_thms = Global_Theory.all_thms_of (Thm.theory_of_thm thm)
     1.8 +    val all_thms = Global_Theory.all_thms_of (Thm.theory_of_thm thm) true
     1.9      fun collect (s, _, _) = if s <> "" then insert (op =) s else I
    1.10      fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE
    1.11      fun resolve_thms names = map_filter (member_of names) all_thms
     2.1 --- a/src/HOL/Mutabelle/mutabelle.ML	Sat Mar 15 11:57:55 2014 +0100
     2.2 +++ b/src/HOL/Mutabelle/mutabelle.ML	Sat Mar 15 11:59:18 2014 +0100
     2.3 @@ -13,23 +13,11 @@
     2.4    val mutate_sign : term -> theory -> (string * string) list -> int -> term list 
     2.5    val mutate_mix : term -> theory -> string list -> 
     2.6     (string * string) list -> int -> term list
     2.7 -
     2.8 -  val all_unconcealed_thms_of : theory -> (string * thm) list
     2.9  end;
    2.10  
    2.11  structure Mutabelle : MUTABELLE = 
    2.12  struct
    2.13  
    2.14 -fun all_unconcealed_thms_of thy =
    2.15 -  let
    2.16 -    val facts = Global_Theory.facts_of thy
    2.17 -  in
    2.18 -    Facts.fold_static
    2.19 -      (fn (s, ths) =>
    2.20 -        if Facts.is_concealed facts s then I else append (map (`(Thm.get_name_hint)) ths))
    2.21 -      facts []
    2.22 -  end;
    2.23 -
    2.24  fun consts_of thy =
    2.25   let
    2.26     val {const_space, constants, ...} = Consts.dest (Sign.consts_of thy)
     3.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Mar 15 11:57:55 2014 +0100
     3.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Mar 15 11:59:18 2014 +0100
     3.3 @@ -336,7 +336,7 @@
     3.4    filter
     3.5      (fn th => (all orelse Context.theory_name (theory_of_thm th) = Context.theory_name thy)
     3.6        (* andalso is_executable_thm thy th *))
     3.7 -    (map snd (filter_out is_forbidden_theorem (Mutabelle.all_unconcealed_thms_of thy)))
     3.8 +    (map snd (filter_out is_forbidden_theorem (Global_Theory.all_thms_of thy false)))
     3.9  
    3.10  fun elapsed_time description e =
    3.11    let val ({elapsed, ...}, result) = Timing.timing e ()
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Mar 15 11:57:55 2014 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Mar 15 11:59:18 2014 +0100
     4.3 @@ -2000,7 +2000,7 @@
     4.4  fun ground_theorem_table thy =
     4.5    fold ((fn @{const Trueprop} $ t1 =>
     4.6              is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
     4.7 -          | _ => I) o prop_of o snd) (Global_Theory.all_thms_of thy) Inttab.empty
     4.8 +          | _ => I) o prop_of o snd) (Global_Theory.all_thms_of thy true) Inttab.empty
     4.9  
    4.10  fun ersatz_table ctxt =
    4.11   #ersatz_table (Data.get (Context.Proof ctxt))
     5.1 --- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Sat Mar 15 11:57:55 2014 +0100
     5.2 +++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Sat Mar 15 11:59:18 2014 +0100
     5.3 @@ -13,17 +13,7 @@
     5.4  structure Find_Unused_Assms : FIND_UNUSED_ASSMS =
     5.5  struct
     5.6  
     5.7 -fun all_unconcealed_thms_of thy =
     5.8 -  let
     5.9 -    val facts = Global_Theory.facts_of thy
    5.10 -  in
    5.11 -    Facts.fold_static
    5.12 -      (fn (s, ths) =>
    5.13 -        if Facts.is_concealed facts s then I else append (map (`(Thm.get_name_hint)) ths))
    5.14 -      facts []
    5.15 -  end
    5.16 -
    5.17 -fun thms_of thy thy_name = all_unconcealed_thms_of thy
    5.18 +fun thms_of thy thy_name = Global_Theory.all_thms_of thy false
    5.19    |> filter (fn (_, th) => Context.theory_name (theory_of_thm th) = thy_name)
    5.20  
    5.21  fun do_while P f s list =
     6.1 --- a/src/Pure/Proof/proof_checker.ML	Sat Mar 15 11:57:55 2014 +0100
     6.2 +++ b/src/Pure/Proof/proof_checker.ML	Sat Mar 15 11:59:18 2014 +0100
     6.3 @@ -16,7 +16,7 @@
     6.4  (***** construct a theorem out of a proof term *****)
     6.5  
     6.6  fun lookup_thm thy =
     6.7 -  let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty in
     6.8 +  let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy true) Symtab.empty in
     6.9      fn s =>
    6.10        (case Symtab.lookup tab s of
    6.11          NONE => error ("Unknown theorem " ^ quote s)
     7.1 --- a/src/Pure/Proof/proof_syntax.ML	Sat Mar 15 11:57:55 2014 +0100
     7.2 +++ b/src/Pure/Proof/proof_syntax.ML	Sat Mar 15 11:59:18 2014 +0100
     7.3 @@ -87,7 +87,7 @@
     7.4  
     7.5  fun proof_of_term thy ty =
     7.6    let
     7.7 -    val thms = Global_Theory.all_thms_of thy;
     7.8 +    val thms = Global_Theory.all_thms_of thy true;
     7.9      val axms = Theory.all_axioms_of thy;
    7.10  
    7.11      fun mk_term t = (if ty then I else map_types (K dummyT))
    7.12 @@ -187,7 +187,7 @@
    7.13  
    7.14  fun cterm_of_proof thy prf =
    7.15    let
    7.16 -    val thm_names = map fst (Global_Theory.all_thms_of thy);
    7.17 +    val thm_names = map fst (Global_Theory.all_thms_of thy true);
    7.18      val axm_names = map fst (Theory.all_axioms_of thy);
    7.19      val thy' = thy
    7.20        |> add_proof_syntax
    7.21 @@ -199,7 +199,7 @@
    7.22  
    7.23  fun read_term thy topsort =
    7.24    let
    7.25 -    val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy));
    7.26 +    val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy true));
    7.27      val axm_names = map fst (Theory.all_axioms_of thy);
    7.28      val ctxt = thy
    7.29        |> add_proof_syntax
     8.1 --- a/src/Pure/global_theory.ML	Sat Mar 15 11:57:55 2014 +0100
     8.2 +++ b/src/Pure/global_theory.ML	Sat Mar 15 11:59:18 2014 +0100
     8.3 @@ -13,7 +13,7 @@
     8.4    val hide_fact: bool -> string -> theory -> theory
     8.5    val get_thms: theory -> xstring -> thm list
     8.6    val get_thm: theory -> xstring -> thm
     8.7 -  val all_thms_of: theory -> (string * thm) list
     8.8 +  val all_thms_of: theory -> bool -> (string * thm) list
     8.9    val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
    8.10    val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list
    8.11    val burrow_facts: ('a list -> 'b list) ->
    8.12 @@ -71,8 +71,13 @@
    8.13  fun get_thm thy xname =
    8.14    Facts.the_single (xname, Position.none) (get_thms thy xname);
    8.15  
    8.16 -fun all_thms_of thy =
    8.17 -  Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) [];
    8.18 +fun all_thms_of thy verbose =
    8.19 +  let
    8.20 +    val facts = facts_of thy;
    8.21 +    fun add (name, ths) =
    8.22 +      if not verbose andalso Facts.is_concealed facts name then I
    8.23 +      else append (map (`(Thm.get_name_hint)) ths);
    8.24 +  in Facts.fold_static add facts [] end;
    8.25  
    8.26  
    8.27