--- a/src/HOL/Eisbach/match_method.ML Tue Jun 02 23:00:50 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML Wed Jun 03 19:25:05 2015 +0200
@@ -181,7 +181,7 @@
val (param_thm', ctxt'') = Thm.proof_attributes atts param_thm ctxt';
fun label_thm thm =
- Thm.cterm_of ctxt' (Free (nm, propT))
+ Thm.cterm_of ctxt'' (Free (nm, propT))
|> Drule.mk_term
|> not (null abs_nms) ? Conjunction.intr thm
@@ -509,19 +509,18 @@
(* Fix schematics in the goal *)
fun focus_concl ctxt i goal =
let
- val ({context, concl, params, prems, asms, schematics}, goal') =
+ val ({context = ctxt', concl, params, prems, asms, schematics}, goal') =
Subgoal.focus_params ctxt i goal;
- val ((_, schematic_terms), context') =
- Variable.import_inst true [Thm.term_of concl] context
- |>> Thm.certify_inst (Thm.theory_of_thm goal');
+ val (inst, ctxt'') = Variable.import_inst true [Thm.term_of concl] ctxt';
+ val (_, schematic_terms) = Thm.certify_inst ctxt'' inst;
val goal'' = Thm.instantiate ([], schematic_terms) goal';
val concl' = Thm.instantiate_cterm ([], schematic_terms) concl;
val (schematic_types, schematic_terms') = schematics;
val schematics' = (schematic_types, schematic_terms @ schematic_terms');
in
- ({context = context', concl = concl', params = params, prems = prems,
+ ({context = ctxt'', concl = concl', params = params, prems = prems,
schematics = schematics', asms = asms} : Subgoal.focus, goal'')
end;
--- a/src/HOL/Import/import_rule.ML Tue Jun 02 23:00:50 2015 +0200
+++ b/src/HOL/Import/import_rule.ML Wed Jun 03 19:25:05 2015 +0200
@@ -328,13 +328,14 @@
fun store_thm binding thm thy =
let
+ val ctxt = Proof_Context.init_global thy
val thm = Drule.export_without_context_open thm
val tvs = Term.add_tvars (Thm.prop_of thm) []
val tns = map (fn (_, _) => "'") tvs
- val nms = fst (fold_map Name.variant tns (Variable.names_of (Proof_Context.init_global thy)))
+ val nms = fst (fold_map Name.variant tns (Variable.names_of ctxt))
val vs = map TVar ((nms ~~ (map (snd o fst) tvs)) ~~ (map snd tvs))
- val cvs = map (Thm.global_ctyp_of thy) vs
- val ctvs = map (Thm.global_ctyp_of thy) (map TVar tvs)
+ val cvs = map (Thm.ctyp_of ctxt) vs
+ val ctvs = map (Thm.ctyp_of ctxt) (map TVar tvs)
val thm' = Thm.instantiate ((ctvs ~~ cvs), []) thm
in
snd (Global_Theory.add_thm ((binding, thm'), []) thy)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Jun 02 23:00:50 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Jun 03 19:25:05 2015 +0200
@@ -947,7 +947,7 @@
val U = TFree ("'u", @{sort type})
val y = Free (yname, U)
val f' = absdummy (U --> T') (Bound 0 $ y)
- val th' = Thm.certify_instantiate
+ val th' = Thm.certify_instantiate ctxt
([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
[((fst (dest_Var f), (U --> T') --> T'), f')]) th
val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th']
@@ -1086,13 +1086,13 @@
if not (fst (dest_Const pred) = fst (dest_Const pred')) then
raise Fail "Trying to instantiate another predicate"
else ()
- in Thm.certify_instantiate (subst_of (pred', pred), []) th end
+ in Thm.certify_instantiate ctxt' (subst_of (pred', pred), []) th end
fun instantiate_ho_args th =
let
val (_, args') =
(strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) th
val ho_args' = map dest_Var (ho_args_of_typ T args')
- in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
+ in Thm.certify_instantiate ctxt' ([], ho_args' ~~ ho_args) th end
val outp_pred =
Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
val ((_, ths'), ctxt1) =
--- a/src/HOL/Tools/Transfer/transfer.ML Tue Jun 02 23:00:50 2015 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Wed Jun 03 19:25:05 2015 +0200
@@ -697,7 +697,7 @@
val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
|> map (fn v as ((a, _), S) => (v, TFree (a, S)))
val thm2 = thm1
- |> Thm.certify_instantiate (instT, [])
+ |> Thm.certify_instantiate ctxt (instT, [])
|> Raw_Simplifier.rewrite_rule ctxt pre_simps
val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
@@ -733,7 +733,7 @@
val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
|> map (fn v as ((a, _), S) => (v, TFree (a, S)))
val thm2 = thm1
- |> Thm.certify_instantiate (instT, [])
+ |> Thm.certify_instantiate ctxt (instT, [])
|> Raw_Simplifier.rewrite_rule ctxt pre_simps
val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
--- a/src/Pure/Isar/code.ML Tue Jun 02 23:00:50 2015 +0200
+++ b/src/Pure/Isar/code.ML Wed Jun 03 19:25:05 2015 +0200
@@ -635,19 +635,19 @@
else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names)
end;
-fun desymbolize_tvars thms =
+fun desymbolize_tvars thy thms =
let
val tvs = fold (Term.add_tvars o Thm.prop_of) thms [];
val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs;
- in map (Thm.certify_instantiate (tvar_subst, [])) thms end;
+ in map (Thm.global_certify_instantiate thy (tvar_subst, [])) thms end;
-fun desymbolize_vars thm =
+fun desymbolize_vars thy thm =
let
val vs = Term.add_vars (Thm.prop_of thm) [];
val var_subst = mk_desymbolization I I Var vs;
- in Thm.certify_instantiate ([], var_subst) thm end;
+ in Thm.global_certify_instantiate thy ([], var_subst) thm end;
-fun canonize_thms thy = desymbolize_tvars #> same_arity thy #> map desymbolize_vars;
+fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy);
(* abstype certificates *)
@@ -706,7 +706,7 @@
in
thm
|> Thm.varifyT_global
- |> Thm.certify_instantiate (inst, [])
+ |> Thm.global_certify_instantiate thy (inst, [])
|> pair subst
end;
@@ -771,7 +771,7 @@
val sorts = map_transpose inter_sorts vss;
val vts = Name.invent_names Name.context Name.aT sorts;
val thms' =
- map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms;
+ map2 (fn vs => Thm.certify_instantiate ctxt (vs ~~ map TFree vts, [])) vss thms;
val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms'))));
fun head_conv ct = if can Thm.dest_comb ct
then Conv.fun_conv head_conv ct
--- a/src/Pure/Isar/proof_context.ML Tue Jun 02 23:00:50 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Jun 03 19:25:05 2015 +0200
@@ -935,7 +935,7 @@
fun comp_hhf_tac ctxt th i st =
PRIMSEQ (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
- (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st;
+ (false, Drule.lift_all ctxt (Thm.cprem_of st i) th, 0) i) st;
fun comp_incr_tac _ [] _ = no_tac
| comp_incr_tac ctxt (th :: ths) i =
--- a/src/Pure/drule.ML Tue Jun 02 23:00:50 2015 +0200
+++ b/src/Pure/drule.ML Wed Jun 03 19:25:05 2015 +0200
@@ -17,7 +17,7 @@
val forall_intr_vars: thm -> thm
val forall_elim_list: cterm list -> thm -> thm
val gen_all: int -> thm -> thm
- val lift_all: cterm -> thm -> thm
+ val lift_all: Proof.context -> cterm -> thm -> thm
val implies_elim_list: thm -> thm list -> thm
val implies_intr_list: cterm list -> thm -> thm
val instantiate_normalize: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
@@ -192,9 +192,12 @@
(*lift vars wrt. outermost goal parameters
-- reverses the effect of gen_all modulo higher-order unification*)
-fun lift_all goal th =
+fun lift_all ctxt raw_goal raw_th =
let
- val thy = Theory.merge (Thm.theory_of_cterm goal, Thm.theory_of_thm th);
+ val thy = Proof_Context.theory_of ctxt;
+ val goal = Thm.transfer_cterm thy raw_goal;
+ val th = Thm.transfer thy raw_th;
+
val maxidx = Thm.maxidx_of th;
val ps = outer_params (Thm.term_of goal)
|> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T));
@@ -204,8 +207,8 @@
|> map (fn (xi, T) => ((xi, T), Term.list_comb (Var (xi, Ts ---> T), ps)));
in
th
- |> Thm.instantiate (Thm.certify_inst thy ([], inst))
- |> fold_rev (Thm.forall_intr o Thm.global_cterm_of thy) ps
+ |> Thm.certify_instantiate ctxt ([], inst)
+ |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) ps
end;
(*direct generalization*)
@@ -225,10 +228,8 @@
| zero_var_indexes_list ths =
let
val thy = Theory.merge_list (map Thm.theory_of_thm ths);
- val inst =
- Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths)
- |> Thm.certify_inst thy;
- in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate inst) ths end;
+ val insts = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths);
+ in map (Thm.adjust_maxidx_thm ~1 o Thm.global_certify_instantiate thy insts) ths end;
val zero_var_indexes = singleton zero_var_indexes_list;
@@ -359,7 +360,7 @@
Context.>>> (Context.map_theory_result (Global_Theory.store_thm_open (name, th)));
fun store_standard_thm name th = store_thm name (export_without_context th);
-fun store_standard_thm_open name thm = store_thm_open name (export_without_context_open thm);
+fun store_standard_thm_open name th = store_thm_open name (export_without_context_open th);
val reflexive_thm =
let val cx = certify (Var(("x",0),TVar(("'a",0),[])))
--- a/src/Pure/more_thm.ML Tue Jun 02 23:00:50 2015 +0200
+++ b/src/Pure/more_thm.ML Wed Jun 03 19:25:05 2015 +0200
@@ -60,10 +60,15 @@
val elim_implies: thm -> thm -> thm
val forall_elim_var: int -> thm -> thm
val forall_elim_vars: int -> thm -> thm
- val certify_inst: theory ->
+ val global_certify_inst: theory ->
((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
(ctyp * ctyp) list * (cterm * cterm) list
- val certify_instantiate:
+ val global_certify_instantiate: theory ->
+ ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
+ val certify_inst: Proof.context ->
+ ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
+ (ctyp * ctyp) list * (cterm * cterm) list
+ val certify_instantiate: Proof.context ->
((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
val forall_intr_frees: thm -> thm
val unvarify_global: thm -> thm
@@ -351,12 +356,19 @@
(* certify_instantiate *)
-fun certify_inst thy (instT, inst) =
+fun global_certify_inst thy (instT, inst) =
(map (fn (v, T) => apply2 (Thm.global_ctyp_of thy) (TVar v, T)) instT,
map (fn (v, t) => apply2 (Thm.global_cterm_of thy) (Var v, t)) inst);
-fun certify_instantiate insts th =
- Thm.instantiate (certify_inst (Thm.theory_of_thm th) insts) th;
+fun global_certify_instantiate thy insts th =
+ Thm.instantiate (global_certify_inst thy insts) th;
+
+fun certify_inst ctxt (instT, inst) =
+ (map (fn (v, T) => apply2 (Thm.ctyp_of ctxt) (TVar v, T)) instT,
+ map (fn (v, t) => apply2 (Thm.cterm_of ctxt) (Var v, t)) inst);
+
+fun certify_instantiate ctxt insts th =
+ Thm.instantiate (certify_inst ctxt insts) th;
(* forall_intr_frees: generalization over all suitable Free variables *)
@@ -375,6 +387,8 @@
fun unvarify_global 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]);
@@ -383,7 +397,7 @@
val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
let val T' = Term_Subst.instantiateT instT T
in (((a, i), T'), Free ((a, T'))) end);
- in certify_instantiate (instT, inst) th end;
+ in global_certify_instantiate thy (instT, inst) th end;
(* close_derivation *)
@@ -444,7 +458,7 @@
val _ = Sign.no_vars ctxt prop;
val (strip, recover, prop') = stripped_sorts thy prop;
val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
- val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.global_ctyp_of thy T, S)) strip;
+ val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of ctxt T, S)) strip;
val thy' = thy
|> Theory.add_axiom ctxt (b, Logic.list_implies (maps Logic.mk_of_sort constraints, prop'));
@@ -461,7 +475,7 @@
fun add_def ctxt unchecked overloaded (b, prop) thy =
let
val _ = Sign.no_vars ctxt prop;
- val prems = map (Thm.global_cterm_of thy) (Logic.strip_imp_prems prop);
+ val prems = map (Thm.cterm_of ctxt) (Logic.strip_imp_prems prop);
val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
val thy' = Theory.add_def ctxt unchecked overloaded (b, concl') thy;
--- a/src/Pure/subgoal.ML Tue Jun 02 23:00:50 2015 +0200
+++ b/src/Pure/subgoal.ML Wed Jun 03 19:25:05 2015 +0200
@@ -31,7 +31,9 @@
fun gen_focus (do_prems, do_concl) ctxt i raw_st =
let
- val st = Simplifier.norm_hhf_protect ctxt raw_st;
+ val st = raw_st
+ |> Thm.transfer (Proof_Context.theory_of ctxt)
+ |> Simplifier.norm_hhf_protect ctxt;
val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
@@ -40,9 +42,8 @@
else ([], goal);
val text = asms @ (if do_concl then [concl] else []);
- val ((_, schematic_terms), ctxt3) =
- Variable.import_inst true (map Thm.term_of text) ctxt2
- |>> Thm.certify_inst (Thm.theory_of_thm raw_st);
+ val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
+ val (_, schematic_terms) = Thm.certify_inst ctxt3 inst;
val schematics = (schematic_types, schematic_terms);
val asms' = map (Thm.instantiate_cterm schematics) asms;
--- a/src/Pure/variable.ML Tue Jun 02 23:00:50 2015 +0200
+++ b/src/Pure/variable.ML Wed Jun 03 19:25:05 2015 +0200
@@ -578,9 +578,8 @@
fun importT ths ctxt =
let
- val thy = Proof_Context.theory_of ctxt;
val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
- val insts' as (instT', _) = Thm.certify_inst thy (instT, []);
+ val insts' as (instT', _) = Thm.certify_inst ctxt' (instT, []);
val ths' = map (Thm.instantiate insts') ths;
in ((instT', ths'), ctxt') end;
@@ -592,9 +591,8 @@
fun import is_open ths ctxt =
let
- val thy = Proof_Context.theory_of ctxt;
val (insts, ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
- val insts' = Thm.certify_inst thy insts;
+ val insts' = Thm.certify_inst ctxt' insts;
val ths' = map (Thm.instantiate insts') ths;
in ((insts', ths'), ctxt') end;
--- a/src/Tools/Code/code_preproc.ML Tue Jun 02 23:00:50 2015 +0200
+++ b/src/Tools/Code/code_preproc.ML Wed Jun 03 19:25:05 2015 +0200
@@ -178,7 +178,7 @@
if eq_list (eq_fst (op =)) (vs_normalized, vs_original)
then (I, ct)
else
- (Thm.certify_instantiate (normalization, []) o Thm.varifyT_global,
+ (Thm.certify_instantiate ctxt (normalization, []) o Thm.varifyT_global,
Thm.cterm_of ctxt (map_types normalize t))
end;