# HG changeset patch # User wenzelm # Date 1491851131 -7200 # Node ID cf504b7a7aa7d2eba9baadcfc18f3b69551b502c # Parent 2bf0d2fcd506443fa1a2b7acc7973c360bb0bfe1 tuned signature; diff -r 2bf0d2fcd506 -r cf504b7a7aa7 src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Mon Apr 10 16:43:12 2017 +0200 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Apr 10 21:05:31 2017 +0200 @@ -332,7 +332,7 @@ fun thms_of all thy = filter - (fn th => (all orelse Thm.theory_name_of_thm th = Context.theory_name thy) + (fn th => (all orelse Thm.theory_name th = Context.theory_name thy) (* andalso is_executable_thm thy th *)) (map snd (filter_out is_forbidden_theorem (Global_Theory.all_thms_of thy false))) diff -r 2bf0d2fcd506 -r cf504b7a7aa7 src/HOL/Nitpick_Examples/Mono_Nits.thy --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Mon Apr 10 16:43:12 2017 +0200 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Mon Apr 10 21:05:31 2017 +0200 @@ -153,7 +153,7 @@ fun theorems_of thy = filter (fn (name, th) => not (is_forbidden_theorem name) andalso - Thm.theory_name_of_thm th = Context.theory_name thy) + Thm.theory_name th = Context.theory_name thy) (Global_Theory.all_thms_of thy true) fun check_formulas tsp = diff -r 2bf0d2fcd506 -r cf504b7a7aa7 src/HOL/Nunchaku/Tools/nunchaku_collect.ML --- a/src/HOL/Nunchaku/Tools/nunchaku_collect.ML Mon Apr 10 16:43:12 2017 +0200 +++ b/src/HOL/Nunchaku/Tools/nunchaku_collect.ML Mon Apr 10 21:05:31 2017 +0200 @@ -556,7 +556,7 @@ #> map snd #> filter (null o fst) #> maps snd - #> filter_out (is_builtin_theory o Thm.theory_id_of_thm) + #> filter_out (is_builtin_theory o Thm.theory_id) #> map Thm.prop_of; fun keys_of _ (ITVal (T, _)) = [key_of_typ T] diff -r 2bf0d2fcd506 -r cf504b7a7aa7 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Mon Apr 10 16:43:12 2017 +0200 +++ b/src/HOL/TPTP/mash_export.ML Mon Apr 10 21:05:31 2017 +0200 @@ -58,7 +58,7 @@ | _ => ("", [])) fun has_thm_thy th thy = - Context.theory_name thy = Thm.theory_name_of_thm th + Context.theory_name thy = Thm.theory_name th fun has_thys thys th = exists (has_thm_thy th) thys @@ -98,7 +98,7 @@ fun do_fact ((_, stature), th) = let val name = nickname_of_thm th - val feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th] + val feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th] val s = encode_str name ^ ": " ^ encode_strs (sort string_ord feats) ^ "\n" in File.append path s @@ -188,14 +188,14 @@ val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name) val isar_deps = isar_dependencies_of name_tabs th val do_query = not (is_bad_query ctxt ho_atp step j th isar_deps) - val goal_feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th] + val goal_feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th] val access_facts = filter_accessible_from th new_facts @ old_facts val (marker, deps) = smart_dependencies_of ctxt params_opt access_facts name_tabs th isar_deps fun extra_features_of (((_, stature), th), weight) = [Thm.prop_of th] - |> features_of ctxt (Thm.theory_name_of_thm th) stature + |> features_of ctxt (Thm.theory_name th) stature |> map (rpair (weight * extra_feature_factor)) val query = @@ -263,7 +263,7 @@ val suggs = old_facts |> filter_accessible_from th - |> mepo_or_mash_suggested_facts ctxt (Thm.theory_name_of_thm th) + |> mepo_or_mash_suggested_facts ctxt (Thm.theory_name th) params max_suggs hyp_ts concl_t |> map (nickname_of_thm o snd) in diff -r 2bf0d2fcd506 -r cf504b7a7aa7 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Apr 10 16:43:12 2017 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Apr 10 21:05:31 2017 +0200 @@ -1360,7 +1360,7 @@ ctxt |> Spec_Rules.get |> filter (curry (op =) Spec_Rules.Unknown o fst) |> maps (snd o snd) - |> filter_out (is_built_in_theory o Thm.theory_id_of_thm) + |> filter_out (is_built_in_theory o Thm.theory_id) |> map (subst_atomic subst o Thm.prop_of) fun arity_of_built_in_const (s, T) = diff -r 2bf0d2fcd506 -r cf504b7a7aa7 src/HOL/Tools/Quickcheck/find_unused_assms.ML --- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Mon Apr 10 16:43:12 2017 +0200 +++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Mon Apr 10 21:05:31 2017 +0200 @@ -15,7 +15,7 @@ fun thms_of thy thy_name = Global_Theory.all_thms_of thy false - |> filter (fn (_, th) => Thm.theory_name_of_thm th = thy_name) + |> filter (fn (_, th) => Thm.theory_name th = thy_name) fun do_while P f s list = if P s then diff -r 2bf0d2fcd506 -r cf504b7a7aa7 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Apr 10 16:43:12 2017 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Apr 10 21:05:31 2017 +0200 @@ -347,7 +347,7 @@ | normalize_eq t = t fun if_thm_before th th' = - if Context.subthy_id (apply2 Thm.theory_id_of_thm (th, th')) then th else th' + if Context.subthy_id (apply2 Thm.theory_id (th, th')) then th else th' (* Hack: Conflate the facts about a class as seen from the outside with the corresponding low-level facts, so that MaSh can learn from the low-level proofs. *) diff -r 2bf0d2fcd506 -r cf504b7a7aa7 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Apr 10 16:43:12 2017 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Apr 10 21:05:31 2017 +0200 @@ -797,7 +797,7 @@ (* There must be a better way to detect local facts. *) (case Long_Name.dest_local hint of SOME suf => - Long_Name.implode [Thm.theory_name_of_thm th, suf, crude_printed_term 25 (Thm.prop_of th)] + Long_Name.implode [Thm.theory_name th, suf, crude_printed_term 25 (Thm.prop_of th)] | NONE => hint) end else @@ -838,7 +838,7 @@ | _ => string_ord (apply2 Context.theory_id_name p)) in fn p => - (case crude_theory_ord (apply2 Thm.theory_id_of_thm p) of + (case crude_theory_ord (apply2 Thm.theory_id p) of EQUAL => (* The hack below is necessary because of odd dependencies that are not reflected in the theory comparison. *) @@ -851,7 +851,7 @@ | ord => ord) end; -val thm_less_eq = Context.subthy_id o apply2 Thm.theory_id_of_thm +val thm_less_eq = Context.subthy_id o apply2 Thm.theory_id fun thm_less p = thm_less_eq p andalso not (thm_less_eq (swap p)) val freezeT = Type.legacy_freeze_type @@ -1124,7 +1124,7 @@ val chunks = app_hd (cons th) chunks val chunks_and_parents' = if thm_less_eq (th, th') andalso - Thm.theory_name_of_thm th = Thm.theory_name_of_thm th' + Thm.theory_name th = Thm.theory_name th' then (chunks, [nickname_of_thm th]) else chunks_and_parents_for chunks th' in @@ -1173,9 +1173,9 @@ | maximal_wrt_access_graph access_G (fact :: facts) = let fun cleanup_wrt (_, th) = - let val thy_id = Thm.theory_id_of_thm th in + let val thy_id = Thm.theory_id th in filter_out (fn (_, th') => - Context.proper_subthy_id (Thm.theory_id_of_thm th', thy_id)) + Context.proper_subthy_id (Thm.theory_id th', thy_id)) end fun shuffle_cleanup accum [] = accum @@ -1229,11 +1229,11 @@ val chained = filter (fn ((_, (scope, _)), _) => scope = Chained) facts - fun fact_has_right_theory (_, th) = thy_name = Thm.theory_name_of_thm th + fun fact_has_right_theory (_, th) = thy_name = Thm.theory_name th fun chained_or_extra_features_of factor (((_, stature), th), weight) = [Thm.prop_of th] - |> features_of ctxt (Thm.theory_name_of_thm th) stature + |> features_of ctxt (Thm.theory_name th) stature |> map (rpair (weight * factor)) in (case get_state ctxt of @@ -1454,7 +1454,7 @@ (learns, (num_nontrivial, next_commit, _)) = let val name = nickname_of_thm th - val feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th] + val feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th] val deps = these (deps_of status th) val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1 val learns = (name, parents, feats, deps) :: learns diff -r 2bf0d2fcd506 -r cf504b7a7aa7 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Mon Apr 10 16:43:12 2017 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Mon Apr 10 21:05:31 2017 +0200 @@ -220,7 +220,7 @@ t fun theory_const_prop_of fudge th = - theory_constify fudge (Thm.theory_name_of_thm th) (Thm.prop_of th) + theory_constify fudge (Thm.theory_name th) (Thm.prop_of th) fun pair_consts_fact thy fudge fact = (case fact |> snd |> theory_const_prop_of fudge |> pconsts_in_fact thy of diff -r 2bf0d2fcd506 -r cf504b7a7aa7 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Mon Apr 10 16:43:12 2017 +0200 +++ b/src/Pure/Isar/proof.ML Mon Apr 10 21:05:31 2017 +0200 @@ -515,7 +515,7 @@ val thy = Proof_Context.theory_of ctxt; val _ = - Context.subthy_id (Thm.theory_id_of_thm goal, Context.theory_id thy) orelse + Context.subthy_id (Thm.theory_id goal, Context.theory_id thy) orelse error "Bad background theory of goal state"; val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal); diff -r 2bf0d2fcd506 -r cf504b7a7aa7 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Mon Apr 10 16:43:12 2017 +0200 +++ b/src/Pure/global_theory.ML Mon Apr 10 21:05:31 2017 +0200 @@ -80,7 +80,7 @@ fold (fn thy' => Symtab.update (Context.theory_name thy', thy')) (Theory.nodes_of thy) Symtab.empty; fun transfer th = - Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_name_of_thm th))) th; + Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_name th))) th; in transfer end; fun all_thms_of thy verbose = diff -r 2bf0d2fcd506 -r cf504b7a7aa7 src/Pure/goal.ML --- a/src/Pure/goal.ML Mon Apr 10 16:43:12 2017 +0200 +++ b/src/Pure/goal.ML Mon Apr 10 21:05:31 2017 +0200 @@ -210,7 +210,7 @@ | SOME st => let val _ = - Context.subthy_id (Thm.theory_id_of_thm st, Context.theory_id thy) orelse + Context.subthy_id (Thm.theory_id st, Context.theory_id thy) orelse err "Bad background theory of goal state"; val res = (finish ctxt' st diff -r 2bf0d2fcd506 -r cf504b7a7aa7 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Mon Apr 10 16:43:12 2017 +0200 +++ b/src/Pure/more_thm.ML Mon Apr 10 21:05:31 2017 +0200 @@ -216,7 +216,7 @@ fun eq_thm_strict ths = eq_thm ths andalso - Context.eq_thy_id (apply2 Thm.theory_id_of_thm ths) andalso + Context.eq_thy_id (apply2 Thm.theory_id ths) andalso op = (apply2 Thm.maxidx_of ths) andalso op = (apply2 Thm.get_tags ths); diff -r 2bf0d2fcd506 -r cf504b7a7aa7 src/Pure/thm.ML --- a/src/Pure/thm.ML Mon Apr 10 16:43:12 2017 +0200 +++ b/src/Pure/thm.ML Mon Apr 10 21:05:31 2017 +0200 @@ -56,8 +56,8 @@ val fold_atomic_cterms: (cterm -> 'a -> 'a) -> thm -> 'a -> 'a val terms_of_tpairs: (term * term) list -> term list val full_prop_of: thm -> term - val theory_id_of_thm: thm -> Context.theory_id - val theory_name_of_thm: thm -> string + val theory_id: thm -> Context.theory_id + val theory_name: thm -> string val maxidx_of: thm -> int val maxidx_thm: thm -> int -> int val shyps_of: thm -> sort Ord_List.T @@ -365,8 +365,8 @@ (* basic components *) val cert_of = #cert o rep_thm; -val theory_id_of_thm = Context.certificate_theory_id o cert_of; -val theory_name_of_thm = Context.theory_id_name o theory_id_of_thm; +val theory_id = Context.certificate_theory_id o cert_of; +val theory_name = Context.theory_id_name o theory_id; val maxidx_of = #maxidx o rep_thm; fun maxidx_thm th i = Int.max (maxidx_of th, i);