--- a/src/HOL/Eisbach/match_method.ML Mon Jul 27 22:44:02 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML Mon Jul 27 23:41:57 2015 +0200
@@ -504,7 +504,7 @@
Subgoal.focus_params ctxt i bindings goal;
val (inst, ctxt'') = Variable.import_inst true [Thm.term_of concl] ctxt';
- val (_, schematic_terms) = Thm.certify_inst ctxt'' inst;
+ val schematic_terms = map (apsnd (Thm.cterm_of ctxt'')) (#2 inst);
val goal'' = Thm.instantiate ([], schematic_terms) goal';
val concl' = Thm.instantiate_cterm ([], schematic_terms) concl;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Jul 27 22:44:02 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Jul 27 23:41:57 2015 +0200
@@ -947,9 +947,11 @@
val U = TFree ("'u", @{sort type})
val y = Free (yname, U)
val f' = absdummy (U --> T') (Bound 0 $ y)
- 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' =
+ Thm.instantiate
+ ([(dest_TVar uninst_T, Thm.ctyp_of ctxt' (U --> T')),
+ (dest_TVar uninst_T', Thm.ctyp_of ctxt' T')],
+ [((fst (dest_Var f), (U --> T') --> T'), Thm.cterm_of ctxt' f')]) th
val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th']
in
th'
@@ -1075,10 +1077,10 @@
val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
handle Type.TYPE_MATCH =>
error ("Type mismatch of predicate " ^ fst (dest_Const pred) ^
- " (trying to match " ^ Syntax.string_of_typ ctxt (fastype_of pred') ^
- " and " ^ Syntax.string_of_typ ctxt (fastype_of pred) ^ ")" ^
- " in " ^ Display.string_of_thm ctxt th)
- in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end
+ " (trying to match " ^ Syntax.string_of_typ ctxt' (fastype_of pred') ^
+ " and " ^ Syntax.string_of_typ ctxt' (fastype_of pred) ^ ")" ^
+ " in " ^ Display.string_of_thm ctxt' th)
+ in map (fn (xi, (S, T)) => ((xi, S), T)) (Vartab.dest subst) end
fun instantiate_typ th =
let
val (pred', _) = strip_intro_concl th
@@ -1086,13 +1088,13 @@
if not (fst (dest_Const pred) = fst (dest_Const pred')) then
raise Fail "Trying to instantiate another predicate"
else ()
- in Thm.certify_instantiate ctxt' (subst_of (pred', pred), []) th end
+ in Thm.instantiate (map (apsnd (Thm.ctyp_of 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 ctxt' ([], ho_args' ~~ ho_args) th end
+ in Thm.instantiate ([], ho_args' ~~ map (Thm.cterm_of ctxt') 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 Mon Jul 27 22:44:02 2015 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Mon Jul 27 23:41:57 2015 +0200
@@ -693,10 +693,11 @@
val err_msg = "Transfer failed to convert goal to an object-logic formula"
val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
val thm1 = Drule.forall_intr_vars thm
- val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
- |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
+ val instT =
+ rev (Term.add_tvars (Thm.full_prop_of thm1) [])
+ |> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S))))
val thm2 = thm1
- |> Thm.certify_instantiate ctxt (instT, [])
+ |> Thm.instantiate (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)
@@ -709,7 +710,7 @@
THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
handle TERM (_, ts) => raise TERM (err_msg, ts)
val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
- val tnames = map (fst o dest_TFree o snd) instT
+ val tnames = map (fst o dest_TFree o Thm.typ_of o snd) instT
in
thm3
|> Raw_Simplifier.rewrite_rule ctxt' post_simps
@@ -729,10 +730,11 @@
val err_msg = "Transfer failed to convert goal to an object-logic formula"
val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
val thm1 = Drule.forall_intr_vars thm
- val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
- |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
+ val instT =
+ rev (Term.add_tvars (Thm.full_prop_of thm1) [])
+ |> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S))))
val thm2 = thm1
- |> Thm.certify_instantiate ctxt (instT, [])
+ |> Thm.instantiate (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)
@@ -745,7 +747,7 @@
THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
handle TERM (_, ts) => raise TERM (err_msg, ts)
val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
- val tnames = map (fst o dest_TFree o snd) instT
+ val tnames = map (fst o dest_TFree o Thm.typ_of o snd) instT
in
thm3
|> Raw_Simplifier.rewrite_rule ctxt' post_simps
--- a/src/Pure/Isar/code.ML Mon Jul 27 22:44:02 2015 +0200
+++ b/src/Pure/Isar/code.ML Mon Jul 27 23:41:57 2015 +0200
@@ -638,14 +638,15 @@
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.global_certify_instantiate thy (tvar_subst, [])) thms end;
+ val instT =
+ mk_desymbolization (unprefix "'") (prefix "'") (Thm.global_ctyp_of thy o TVar) tvs;
+ in map (Thm.instantiate (instT, [])) thms end;
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.global_certify_instantiate thy ([], var_subst) thm end;
+ val inst = mk_desymbolization I I (Thm.global_cterm_of thy o Var) vs;
+ in Thm.instantiate ([], inst) thm end;
fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy);
@@ -700,13 +701,13 @@
val mapping = map2 (fn (v, sort) => fn sort' =>
(v, Sorts.inter_sort (Sign.classes_of thy) (sort, sort'))) vs sorts;
val inst = map2 (fn (v, sort) => fn (_, sort') =>
- (((v, 0), sort), TFree (v, sort'))) vs mapping;
+ (((v, 0), sort), Thm.global_ctyp_of thy (TFree (v, sort')))) vs mapping;
val subst = (map_types o map_type_tfree)
(fn (v, _) => TFree (v, the (AList.lookup (op =) mapping v)));
in
thm
|> Thm.varifyT_global
- |> Thm.global_certify_instantiate thy (inst, [])
+ |> Thm.instantiate (inst, [])
|> pair subst
end;
@@ -771,7 +772,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 ctxt (vs ~~ map TFree vts, [])) vss thms;
+ map2 (fn vs => Thm.instantiate (vs ~~ map (Thm.ctyp_of ctxt o 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/subgoal.ML Mon Jul 27 22:44:02 2015 +0200
+++ b/src/Pure/Isar/subgoal.ML Mon Jul 27 23:41:57 2015 +0200
@@ -55,7 +55,7 @@
val text = asms @ (if do_concl then [concl] else []);
val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
- val (_, schematic_terms) = Thm.certify_inst ctxt3 inst;
+ val schematic_terms = map (apsnd (Thm.cterm_of ctxt3)) (#2 inst);
val schematics = (schematic_types, schematic_terms);
val asms' = map (Thm.instantiate_cterm schematics) asms;
--- a/src/Pure/drule.ML Mon Jul 27 22:44:02 2015 +0200
+++ b/src/Pure/drule.ML Mon Jul 27 23:41:57 2015 +0200
@@ -206,10 +206,10 @@
val Ts = map Term.fastype_of ps;
val inst =
Thm.fold_terms Term.add_vars th []
- |> map (fn (xi, T) => ((xi, T), Term.list_comb (Var (xi, Ts ---> T), ps)));
+ |> map (fn (xi, T) => ((xi, T), Thm.cterm_of ctxt (Term.list_comb (Var (xi, Ts ---> T), ps))));
in
th
- |> Thm.certify_instantiate ctxt ([], inst)
+ |> Thm.instantiate ([], inst)
|> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) ps
end;
@@ -230,8 +230,11 @@
| zero_var_indexes_list ths =
let
val thy = Theory.merge_list (map Thm.theory_of_thm ths);
- 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 (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths);
+ val insts' =
+ (map (apsnd (Thm.global_ctyp_of thy)) instT,
+ map (apsnd (Thm.global_cterm_of thy)) inst);
+ in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate insts') ths end;
val zero_var_indexes = singleton zero_var_indexes_list;
--- a/src/Pure/more_thm.ML Mon Jul 27 22:44:02 2015 +0200
+++ b/src/Pure/more_thm.ML Mon Jul 27 23:41:57 2015 +0200
@@ -61,16 +61,6 @@
val forall_elim_var: int -> thm -> thm
val forall_elim_vars: int -> thm -> thm
val instantiate': ctyp option list -> cterm option list -> thm -> thm
- val global_certify_inst: theory ->
- ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
- ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
- 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 ->
- ((indexname * sort) * ctyp) list * ((indexname * typ) * 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
val close_derivation: thm -> thm
@@ -375,23 +365,6 @@
in thm'' end;
-(* certify_instantiate *)
-
-fun global_certify_inst thy (instT, inst) =
- (map (apsnd (Thm.global_ctyp_of thy)) instT,
- map (apsnd (Thm.global_cterm_of thy)) inst);
-
-fun global_certify_instantiate thy insts th =
- Thm.instantiate (global_certify_inst thy insts) th;
-
-fun certify_inst ctxt (instT, inst) =
- (map (apsnd (Thm.ctyp_of ctxt)) instT,
- map (apsnd (Thm.cterm_of ctxt)) inst);
-
-fun certify_instantiate ctxt insts th =
- Thm.instantiate (certify_inst ctxt insts) th;
-
-
(* forall_intr_frees: generalization over all suitable Free variables *)
fun forall_intr_frees th =
@@ -417,8 +390,8 @@
val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
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 global_certify_instantiate thy (instT, inst) th end;
+ 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;
(* close_derivation *)
--- a/src/Pure/variable.ML Mon Jul 27 22:44:02 2015 +0200
+++ b/src/Pure/variable.ML Mon Jul 27 23:41:57 2015 +0200
@@ -600,8 +600,8 @@
fun importT ths ctxt =
let
val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
- val insts' as (instT', _) = Thm.certify_inst ctxt' (instT, []);
- val ths' = map (Thm.instantiate insts') ths;
+ val instT' = map (apsnd (Thm.ctyp_of ctxt')) instT;
+ val ths' = map (Thm.instantiate (instT', [])) ths;
in ((instT', ths'), ctxt') end;
fun import_prf is_open prf ctxt =
@@ -612,8 +612,10 @@
fun import is_open ths ctxt =
let
- val (insts, ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
- val insts' = Thm.certify_inst ctxt' insts;
+ val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
+ val insts' =
+ (map (apsnd (Thm.ctyp_of ctxt')) instT,
+ map (apsnd (Thm.cterm_of ctxt')) inst);
val ths' = map (Thm.instantiate insts') ths;
in ((insts', ths'), ctxt') end;
--- a/src/Tools/Code/code_preproc.ML Mon Jul 27 22:44:02 2015 +0200
+++ b/src/Tools/Code/code_preproc.ML Mon Jul 27 23:41:57 2015 +0200
@@ -168,17 +168,19 @@
fun normalized_tfrees_sandwich ctxt ct =
let
val t = Thm.term_of ct;
- val vs_original = fold_term_types (K (fold_atyps (insert (eq_fst op =)
- o dest_TFree))) t [];
+ val vs_original =
+ fold_term_types (K (fold_atyps (insert (eq_fst op =) o dest_TFree))) t [];
val vs_normalized = Name.invent_names Name.context Name.aT (map snd vs_original);
- val normalize = map_type_tfree (TFree o the o AList.lookup (op =) (vs_original ~~ vs_normalized));
+ val normalize =
+ map_type_tfree (TFree o the o AList.lookup (op =) (vs_original ~~ vs_normalized));
val normalization =
- map2 (fn (v, sort) => fn (v', _) => (((v', 0), sort), TFree (v, sort))) vs_original vs_normalized;
+ map2 (fn (v, sort) => fn (v', _) => (((v', 0), sort), Thm.ctyp_of ctxt (TFree (v, sort))))
+ vs_original vs_normalized;
in
if eq_list (eq_fst (op =)) (vs_normalized, vs_original)
then (I, ct)
else
- (Thm.certify_instantiate ctxt (normalization, []) o Thm.varifyT_global,
+ (Thm.instantiate (normalization, []) o Thm.varifyT_global,
Thm.cterm_of ctxt (map_types normalize t))
end;