--- 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)))
--- 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 =
--- 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]
--- 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
--- 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) =
--- 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
--- 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. *)
--- 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
--- 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
--- 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);
--- 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 =
--- 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
--- 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);
--- 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);