# HG changeset patch
# User wenzelm
# Date 1435926775 -7200
# Node ID 16d80e5ef2dc40e62764d1f8b28f9e072cacd3e2
# Parent  22830a64358f2c7ba5a6ab2e2da6e94934c480a6
tuned signature;

diff -r 22830a64358f -r 16d80e5ef2dc src/HOL/Mutabelle/mutabelle_extra.ML
--- 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)))
 
diff -r 22830a64358f -r 16d80e5ef2dc src/HOL/Nitpick_Examples/Mono_Nits.thy
--- 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 =
diff -r 22830a64358f -r 16d80e5ef2dc src/HOL/TPTP/mash_export.ML
--- 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
 
diff -r 22830a64358f -r 16d80e5ef2dc src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- 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
diff -r 22830a64358f -r 16d80e5ef2dc src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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]
diff -r 22830a64358f -r 16d80e5ef2dc src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- 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
diff -r 22830a64358f -r 16d80e5ef2dc src/Pure/thm.ML
--- 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;