# HG changeset patch
# User wenzelm
# Date 1438112823 -7200
# Node ID bacfb7c45d8151a1d92506a70b2e414d26dea4ce
# Parent  81bddc4832e698f0f4bcd3727d8d8cf452be9a2a
more explicit context;
tuned signature;

diff -r 81bddc4832e6 -r bacfb7c45d81 src/HOL/Library/old_recdef.ML
--- a/src/HOL/Library/old_recdef.ML	Tue Jul 28 21:31:16 2015 +0200
+++ b/src/HOL/Library/old_recdef.ML	Tue Jul 28 21:47:03 2015 +0200
@@ -2625,7 +2625,8 @@
 
 fun simplify_defn ctxt strict congs wfs pats def0 =
   let
-    val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq
+    val thy = Proof_Context.theory_of ctxt;
+    val def = Thm.unvarify_global thy def0 RS meta_eq_to_obj_eq
     val {rules, rows, TCs, full_pats_TCs} = Prim.post_definition ctxt congs (def, pats)
     val {lhs=f,rhs} = USyntax.dest_eq (concl def)
     val (_,[R,_]) = USyntax.strip_comb rhs
diff -r 81bddc4832e6 -r bacfb7c45d81 src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Tue Jul 28 21:31:16 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Tue Jul 28 21:47:03 2015 +0200
@@ -27,7 +27,7 @@
   let
     val thms as thm1 :: _ = raw_thms
       |> Conjunction.intr_balanced
-      |> Thm.unvarify_global
+      |> Thm.unvarify_global thy
       |> Conjunction.elim_balanced (length raw_thms)
       |> map Simpdata.mk_meta_eq
       |> map Drule.zero_var_indexes;
@@ -53,7 +53,7 @@
     fun true_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term True});
     fun false_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term False});
 
-    val monomorphic_prop_of = Thm.prop_of o Thm.unvarify_global o Drule.zero_var_indexes;
+    val monomorphic_prop_of = Thm.prop_of o Thm.unvarify_global thy o Drule.zero_var_indexes;
 
     fun massage_inject (tp $ (eqv $ (_ $ t $ u) $ rhs)) = tp $ (eqv $ mk_fcT_eq (t, u) $ rhs);
     fun massage_distinct (tp $ (_ $ (_ $ t $ u))) = [tp $ false_eq (t, u), tp $ false_eq (u, t)];
diff -r 81bddc4832e6 -r bacfb7c45d81 src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Tue Jul 28 21:31:16 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Tue Jul 28 21:47:03 2015 +0200
@@ -35,12 +35,13 @@
 
 fun find_unused_assms ctxt thy_name =
   let
+    val thy = Proof_Context.theory_of ctxt
     val ctxt' = ctxt
        |> Config.put Quickcheck.abort_potential true
        |> Config.put Quickcheck.quiet true
     val all_thms =
       filter (fn (s, _) => length (Long_Name.explode s) = 2)  (* FIXME !? *)
-        (thms_of (Proof_Context.theory_of ctxt) thy_name)
+        (thms_of thy thy_name)
     fun check_single conjecture =
       (case try (Quickcheck.test_terms ctxt' (true, true) []) [(conjecture, [])] of
         SOME (SOME _) => false
@@ -53,7 +54,7 @@
             if member (op =) S x then I
             else insert (eq_set (op =)) (insert (op =) x S)) X) Ss []
     fun check (s, th) =
-      (case Logic.strip_horn (Thm.prop_of (Thm.unvarify_global th)) of
+      (case Logic.strip_horn (Thm.prop_of (Thm.unvarify_global thy th)) of
         ([], _) => (s, NONE)
       | (ts, t) =>
           let
diff -r 81bddc4832e6 -r bacfb7c45d81 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Tue Jul 28 21:31:16 2015 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Tue Jul 28 21:47:03 2015 +0200
@@ -178,7 +178,7 @@
           else ()
       in
         arg
-        |> apsnd Thm.unvarify_global
+        |> apsnd (Thm.unvarify_global thy)
         |> process_all (zip3 alt_names rew_imps frees)
       end
 
diff -r 81bddc4832e6 -r bacfb7c45d81 src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Tue Jul 28 21:31:16 2015 +0200
+++ b/src/Pure/conjunction.ML	Tue Jul 28 21:47:03 2015 +0200
@@ -76,8 +76,7 @@
 val A_B = read_prop "A &&& B";
 
 val conjunction_def =
-  Thm.unvarify_global
-    (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def");
+  Thm.unvarify_axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def";
 
 fun conjunctionD which =
   Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
diff -r 81bddc4832e6 -r bacfb7c45d81 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Jul 28 21:31:16 2015 +0200
+++ b/src/Pure/drule.ML	Tue Jul 28 21:47:03 2015 +0200
@@ -566,7 +566,7 @@
 
 local
   val A = certify (Free ("A", propT));
-  val axiom = Thm.unvarify_global o Thm.axiom (Context.the_theory (Context.the_thread_data ()));
+  val axiom = Thm.unvarify_axiom (Context.the_theory (Context.the_thread_data ()));
   val prop_def = axiom "Pure.prop_def";
   val term_def = axiom "Pure.term_def";
   val sort_constraint_def = axiom "Pure.sort_constraint_def";
@@ -640,7 +640,7 @@
   store_standard_thm (Binding.concealed (Binding.make ("sort_constraint_eq", @{here})))
     (Thm.equal_intr
       (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA)
-        (Thm.unvarify_global sort_constraintI)))
+        (Thm.unvarify_global (Context.the_theory (Context.the_thread_data ())) sort_constraintI)))
       (implies_intr_list [A, C] (Thm.assume A)));
 
 end;
diff -r 81bddc4832e6 -r bacfb7c45d81 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Jul 28 21:31:16 2015 +0200
+++ b/src/Pure/more_thm.ML	Tue Jul 28 21:47:03 2015 +0200
@@ -63,7 +63,8 @@
   val forall_elim_vars: int -> thm -> thm
   val instantiate': ctyp option list -> cterm option list -> thm -> thm
   val forall_intr_frees: thm -> thm
-  val unvarify_global: thm -> thm
+  val unvarify_global: theory -> thm -> thm
+  val unvarify_axiom: theory -> string -> thm
   val close_derivation: thm -> thm
   val rename_params_rule: string list * int -> thm -> thm
   val rename_boundvars: term -> term -> thm -> thm
@@ -376,10 +377,8 @@
 
 (* unvarify_global: global schematic variables *)
 
-fun unvarify_global th =
+fun unvarify_global thy th =
   let
-    val thy = Thm.theory_of_thm th;
-
     val prop = Thm.full_prop_of th;
     val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th)
       handle TERM (msg, _) => raise THM (msg, 0, [th]);
@@ -390,6 +389,8 @@
       in (((a, i), T'), Thm.global_cterm_of thy (Free ((a, T')))) end);
   in Thm.instantiate (map (apsnd (Thm.global_ctyp_of thy)) instT, inst) th end;
 
+fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy;
+
 
 (* close_derivation *)
 
@@ -459,7 +460,7 @@
     val axm' = Thm.axiom thy' axm_name;
     val thm =
       Thm.instantiate (recover, []) axm'
-      |> unvarify_global
+      |> unvarify_global thy'
       |> fold elim_implies of_sorts;
   in ((axm_name, thm), thy') end;
 
@@ -476,7 +477,7 @@
     val axm' = Thm.axiom thy' axm_name;
     val thm =
       Thm.instantiate (recover, []) axm'
-      |> unvarify_global
+      |> unvarify_global thy'
       |> fold_rev Thm.implies_intr prems;
   in ((axm_name, thm), thy') end;