--- a/src/HOL/Mutabelle/mutabelle_extra.ML Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Jul 03 14:32:55 2015 +0200
@@ -332,7 +332,7 @@
fun thms_of all thy =
filter
- (fn th => (all orelse Context.theory_name (Thm.theory_of_thm th) = Context.theory_name thy)
+ (fn th => (all orelse Thm.theory_name_of_thm 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 Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Fri Jul 03 14:32:55 2015 +0200
@@ -153,7 +153,7 @@
fun theorems_of thy =
filter (fn (name, th) =>
not (is_forbidden_theorem name) andalso
- (Thm.theory_of_thm th, thy) |> apply2 Context.theory_name |> op =)
+ Thm.theory_name_of_thm th = Context.theory_name thy)
(Global_Theory.all_thms_of thy true)
fun check_formulas tsp =
--- a/src/HOL/TPTP/mash_export.ML Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/TPTP/mash_export.ML Fri Jul 03 14:32:55 2015 +0200
@@ -58,7 +58,7 @@
| _ => ("", []))
fun has_thm_thy th thy =
- Context.theory_name thy = Context.theory_name (Thm.theory_of_thm th)
+ Context.theory_name thy = Thm.theory_name_of_thm th
fun has_thys thys th = exists (has_thm_thy th) thys
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Fri Jul 03 14:32:55 2015 +0200
@@ -13,8 +13,9 @@
structure Find_Unused_Assms : FIND_UNUSED_ASSMS =
struct
-fun thms_of thy thy_name = Global_Theory.all_thms_of thy false
- |> filter (fn (_, th) => Context.theory_name (Thm.theory_of_thm th) = thy_name)
+fun thms_of thy thy_name =
+ Global_Theory.all_thms_of thy false
+ |> filter (fn (_, th) => Thm.theory_name_of_thm th = thy_name)
fun do_while P f s list =
if P s then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 03 14:32:55 2015 +0200
@@ -740,14 +740,12 @@
fun elided_backquote_thm threshold th =
elide_string threshold (backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th)
-val thy_name_of_thm = Context.theory_name o Thm.theory_of_thm
-
fun nickname_of_thm th =
if Thm.has_name_hint th then
let val hint = Thm.get_name_hint th in
(* There must be a better way to detect local facts. *)
(case Long_Name.dest_local hint of
- SOME suf => Long_Name.implode [thy_name_of_thm th, suf, elided_backquote_thm 50 th]
+ SOME suf => Long_Name.implode [Thm.theory_name_of_thm th, suf, elided_backquote_thm 50 th]
| NONE => hint)
end
else
@@ -1073,10 +1071,10 @@
let
val chunks = app_hd (cons th) chunks
val chunks_and_parents' =
- if thm_less_eq (th, th') andalso thy_name_of_thm th = thy_name_of_thm th' then
- (chunks, [nickname_of_thm th])
- else
- chunks_and_parents_for chunks th'
+ if thm_less_eq (th, th') andalso
+ Thm.theory_name_of_thm th = Thm.theory_name_of_thm th'
+ then (chunks, [nickname_of_thm th])
+ else chunks_and_parents_for chunks th'
in
(parents, fact) :: do_facts chunks_and_parents' facts
end
@@ -1158,8 +1156,7 @@
val chained = filter (fn ((_, (scope, _)), _) => scope = Chained) facts
- fun fact_has_right_theory (_, th) =
- thy_name = Context.theory_name (Thm.theory_of_thm th)
+ fun fact_has_right_theory (_, th) = thy_name = Thm.theory_name_of_thm th
fun chained_or_extra_features_of factor (((_, stature), th), weight) =
[Thm.prop_of th]
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Fri Jul 03 14:32:55 2015 +0200
@@ -220,7 +220,7 @@
t
fun theory_const_prop_of fudge th =
- theory_constify fudge (Context.theory_name (Thm.theory_of_thm th)) (Thm.prop_of th)
+ theory_constify fudge (Thm.theory_name_of_thm 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/thm.ML Thu Jul 02 16:14:20 2015 +0200
+++ b/src/Pure/thm.ML Fri Jul 03 14:32:55 2015 +0200
@@ -70,6 +70,7 @@
val terms_of_tpairs: (term * term) list -> term list
val full_prop_of: thm -> term
val theory_of_thm: thm -> theory
+ val theory_name_of_thm: thm -> string
val maxidx_of: thm -> int
val maxidx_thm: thm -> int -> int
val hyps_of: thm -> term list
@@ -391,6 +392,7 @@
(* basic components *)
val theory_of_thm = #thy o rep_thm;
+val theory_name_of_thm = Context.theory_name o #thy o rep_thm;
val maxidx_of = #maxidx o rep_thm;
fun maxidx_thm th i = Int.max (maxidx_of th, i);
val hyps_of = #hyps o rep_thm;