--- 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
--- 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)];
--- 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
--- 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
--- 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
--- 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;
--- 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;