--- a/src/HOL/Decision_Procs/Approximation.thy Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Tue Mar 03 19:08:04 2015 +0100
@@ -3641,16 +3641,16 @@
|> HOLogic.dest_list
val p = prec
|> HOLogic.mk_number @{typ nat}
- |> Thm.cterm_of (Proof_Context.theory_of ctxt)
+ |> Proof_Context.cterm_of ctxt
in case taylor
of NONE => let
val n = vs |> length
|> HOLogic.mk_number @{typ nat}
- |> Thm.cterm_of (Proof_Context.theory_of ctxt)
+ |> Proof_Context.cterm_of ctxt
val s = vs
|> map lookup_splitting
|> HOLogic.mk_list @{typ nat}
- |> Thm.cterm_of (Proof_Context.theory_of ctxt)
+ |> Proof_Context.cterm_of ctxt
in
(rtac (Thm.instantiate ([], [(@{cpat "?n::nat"}, n),
(@{cpat "?prec::nat"}, p),
@@ -3663,9 +3663,9 @@
else let
val t = t
|> HOLogic.mk_number @{typ nat}
- |> Thm.cterm_of (Proof_Context.theory_of ctxt)
+ |> Proof_Context.cterm_of ctxt
val s = vs |> map lookup_splitting |> hd
- |> Thm.cterm_of (Proof_Context.theory_of ctxt)
+ |> Proof_Context.cterm_of ctxt
in
rtac (Thm.instantiate ([], [(@{cpat "?s::nat"}, s),
(@{cpat "?t::nat"}, t),
--- a/src/HOL/Decision_Procs/Ferrack.thy Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Tue Mar 03 19:08:04 2015 +0100
@@ -1999,7 +1999,7 @@
let
val vs = Term.add_frees t [];
val t' = (term_of_fm vs o @{code linrqe} o fm_of_term vs) t;
- in (Thm.cterm_of (Proof_Context.theory_of ctxt) o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
+ in (Proof_Context.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
end;
*}
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Mar 03 19:08:04 2015 +0100
@@ -4155,7 +4155,7 @@
in
fn (ctxt, alternative, ty, ps, ct) =>
- cterm_of (Proof_Context.theory_of ctxt)
+ Proof_Context.cterm_of ctxt
(frpar_procedure alternative ty ps (term_of ct))
end
--- a/src/HOL/Decision_Procs/approximation.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Decision_Procs/approximation.ML Tue Mar 03 19:08:04 2015 +0100
@@ -92,7 +92,7 @@
in t end
fun apply_tactic ctxt term tactic =
- cterm_of (Proof_Context.theory_of ctxt) term
+ Proof_Context.cterm_of ctxt term
|> Goal.init
|> SINGLE tactic
|> the |> prems_of |> hd
@@ -120,7 +120,7 @@
|> foldr1 HOLogic.mk_conj))
fun approx_arith prec ctxt t = realify t
- |> Thm.cterm_of (Proof_Context.theory_of ctxt)
+ |> Proof_Context.cterm_of ctxt
|> Reification.conv ctxt form_equations
|> prop_of
|> Logic.dest_equals |> snd
--- a/src/HOL/Library/Old_SMT/old_smt_utils.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_utils.ML Tue Mar 03 19:08:04 2015 +0100
@@ -161,7 +161,7 @@
(* certified terms *)
-fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt)
+fun certify ctxt = Proof_Context.cterm_of ctxt
fun typ_of ct = #T (Thm.rep_cterm ct)
--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML Tue Mar 03 19:08:04 2015 +0100
@@ -114,7 +114,7 @@
val parse_id = Scan.one Symbol.is_letter ::: Scan.many Symbol.is_letdig >> implode
fun parse_varpow ctxt = parse_id -- Scan.optional (str "^" |-- nat) 1 >>
- (fn (x, k) => (cterm_of (Proof_Context.theory_of ctxt) (Free (x, @{typ real})), k))
+ (fn (x, k) => (Proof_Context.cterm_of ctxt (Free (x, @{typ real})), k))
fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
(fn xs => fold FuncUtil.Ctermfunc.update xs FuncUtil.Ctermfunc.empty)
--- a/src/HOL/Library/simps_case_conv.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Library/simps_case_conv.ML Tue Mar 03 19:08:04 2015 +0100
@@ -97,7 +97,7 @@
| import (thm :: thms) ctxt =
let
val fun_ct = strip_eq #> fst #> strip_comb #> fst #> Logic.mk_term
- #> Thm.cterm_of (Proof_Context.theory_of ctxt)
+ #> Proof_Context.cterm_of ctxt
val ct = fun_ct thm
val cts = map fun_ct thms
val pairs = map (fn s => (s,ct)) cts
--- a/src/HOL/Multivariate_Analysis/normarith.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Tue Mar 03 19:08:04 2015 +0100
@@ -344,7 +344,7 @@
fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
fun mk_norm t = Thm.apply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
fun mk_equals l r = Thm.apply (Thm.apply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
- val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (cterm_of (Proof_Context.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns
+ val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (Proof_Context.cterm_of ctxt' (Free(n,@{typ real}))))) lctab fxns
val replace_conv = try_conv (rewrs_conv asl)
val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv))
val ges' =
--- a/src/HOL/Nominal/nominal_induct.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML Tue Mar 03 19:08:04 2015 +0100
@@ -54,7 +54,7 @@
end;
val substs =
map2 subst insts concls |> flat |> distinct (op =)
- |> map (apply2 (Thm.cterm_of (Proof_Context.theory_of ctxt)));
+ |> map (apply2 (Proof_Context.cterm_of ctxt));
in
(((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule)
end;
--- a/src/HOL/Nominal/nominal_primrec.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Tue Mar 03 19:08:04 2015 +0100
@@ -281,7 +281,7 @@
val qualify = Binding.qualify false
(space_implode "_" (map (Long_Name.base_name o #1) defs));
val names_atts' = map (apfst qualify) names_atts;
- val cert = cterm_of (Proof_Context.theory_of lthy');
+ val cert = Proof_Context.cterm_of lthy';
fun mk_idx eq =
let
--- a/src/HOL/Tools/BNF/bnf_def.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML Tue Mar 03 19:08:04 2015 +0100
@@ -1227,11 +1227,11 @@
val funTs = map (fn T => bdT --> T) ranTs;
val ran_bnfT = mk_bnf_T ranTs Calpha;
val (revTs, Ts) = `rev (bd_bnfT :: funTs);
- val cTs = map (SOME o certifyT lthy) [ran_bnfT, Library.foldr1 HOLogic.mk_prodT Ts];
+ val cTs = map (SOME o Proof_Context.ctyp_of lthy) [ran_bnfT, Library.foldr1 HOLogic.mk_prodT Ts];
val tinst = fold (fn T => fn t => HOLogic.mk_split (Term.absdummy T t)) (tl revTs)
(Term.absdummy (hd revTs) (Term.list_comb (mk_bnf_map bdTs ranTs,
map Bound (live - 1 downto 0)) $ Bound live));
- val cts = [NONE, SOME (certify lthy tinst)];
+ val cts = [NONE, SOME (Proof_Context.cterm_of lthy tinst)];
in
Drule.instantiate' cTs cts @{thm surj_imp_ordLeq}
end);
@@ -1346,7 +1346,7 @@
fun mk_rel_flip () =
let
val rel_conversep_thm = Lazy.force rel_conversep;
- val cts = map (SOME o certify lthy) Rs;
+ val cts = map (SOME o Proof_Context.cterm_of lthy) Rs;
val rel_conversep_thm' = cterm_instantiate_pos cts rel_conversep_thm;
in
unfold_thms lthy @{thms conversep_iff} (rel_conversep_thm' RS @{thm predicate2_eqD})
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Mar 03 19:08:04 2015 +0100
@@ -476,7 +476,7 @@
let
val Rs = Term.add_vars (prop_of thm) [];
val Rs' = rev (drop (length Rs - n) Rs);
- val cRs = map (fn f => (certify lthy (Var f), certify lthy (mk_flip f))) Rs';
+ val cRs = map (fn f => (Proof_Context.cterm_of lthy (Var f), Proof_Context.cterm_of lthy (mk_flip f))) Rs';
in
Drule.cterm_instantiate cRs thm
end;
@@ -598,14 +598,14 @@
Drule.dummy_thm
else
let val ctor' = mk_ctor Bs ctor in
- cterm_instantiate_pos [NONE, NONE, SOME (certify lthy ctor')] arg_cong
+ cterm_instantiate_pos [NONE, NONE, SOME (Proof_Context.cterm_of lthy ctor')] arg_cong
end;
fun mk_cIn ctor k xs =
let val absT = domain_type (fastype_of ctor) in
mk_absumprod absT abs n k xs
|> fp = Greatest_FP ? curry (op $) ctor
- |> certify lthy
+ |> Proof_Context.cterm_of lthy
end;
val cxIns = map2 (mk_cIn ctor) ks xss;
@@ -615,7 +615,7 @@
fold_thms lthy [ctr_def']
(unfold_thms lthy (o_apply :: pre_map_def ::
(if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_map @ abs_inverses)
- (cterm_instantiate_pos (map (SOME o certify lthy) fs @ [SOME cxIn])
+ (cterm_instantiate_pos (map (SOME o Proof_Context.cterm_of lthy) fs @ [SOME cxIn])
(if fp = Least_FP then fp_map_thm
else fp_map_thm RS ctor_cong RS (ctor_dtor RS sym RS trans))))
|> singleton (Proof_Context.export names_lthy lthy);
@@ -643,7 +643,7 @@
(unfold_thms lthy (pre_rel_def :: abs_inverses @
(if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @
@{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]})
- (cterm_instantiate_pos (map (SOME o certify lthy) Rs @ [SOME cxIn, SOME cyIn])
+ (cterm_instantiate_pos (map (SOME o Proof_Context.cterm_of lthy) Rs @ [SOME cxIn, SOME cyIn])
fp_rel_thm))
|> postproc
|> singleton (Proof_Context.export names_lthy lthy);
@@ -734,7 +734,7 @@
val goal = Logic.mk_implies (mk_Trueprop_mem (elem, set $ ta), thesis);
val thm =
Goal.prove_sorry lthy [] (flat premss) goal (fn {context = ctxt, prems} =>
- mk_set_cases_tac ctxt (certify ctxt ta) prems exhaust set_thms)
+ mk_set_cases_tac ctxt (Proof_Context.cterm_of ctxt ta) prems exhaust set_thms)
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
|> rotate_prems ~1;
@@ -812,7 +812,7 @@
fun prove goal =
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
- mk_rel_sel_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust (flat disc_thmss)
+ mk_rel_sel_tac ctxt (Proof_Context.cterm_of ctxt ta) (Proof_Context.cterm_of ctxt tb) exhaust (flat disc_thmss)
(flat sel_thmss) rel_inject_thms distincts rel_distinct_thms live_nesting_rel_eqs)
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation;
@@ -846,7 +846,7 @@
val goal = Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms, thesis);
val thm =
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
- mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust injects
+ mk_rel_cases_tac ctxt (Proof_Context.cterm_of ctxt ta) (Proof_Context.cterm_of ctxt tb) exhaust injects
rel_inject_thms distincts rel_distinct_thms live_nesting_rel_eqs)
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation;
@@ -920,7 +920,7 @@
else
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
- mk_map_disc_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss) map_thms)
+ mk_map_disc_iff_tac ctxt (Proof_Context.cterm_of ctxt ta) exhaust (flat disc_thmss) map_thms)
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
|> map Thm.close_derivation
@@ -954,7 +954,7 @@
else
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
- mk_map_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss) map_thms
+ mk_map_sel_tac ctxt (Proof_Context.cterm_of ctxt ta) exhaust (flat disc_thmss) map_thms
(flat sel_thmss) live_nesting_map_id0s)
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
@@ -1013,7 +1013,7 @@
else
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
- mk_set_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
+ mk_set_sel_tac ctxt (Proof_Context.cterm_of ctxt ta) exhaust (flat disc_thmss)
(flat sel_thmss) set0_thms)
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
@@ -1302,7 +1302,7 @@
val rel_induct0_thm =
Goal.prove_sorry lthy [] prems goal (fn {context = ctxt, prems} =>
- mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (certify ctxt) IRs) exhausts ctor_defss
+ mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (Proof_Context.cterm_of ctxt) IRs) exhausts ctor_defss
ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs)
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation;
@@ -1560,7 +1560,7 @@
val rel_coinduct0_thm =
Goal.prove_sorry lthy [] prems goal (fn {context = ctxt, prems} =>
- mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (certify ctxt) IRs) prems
+ mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (Proof_Context.cterm_of ctxt) IRs) prems
(map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars)
(map (flat o #sel_thmss) ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects
rel_pre_defs abs_inverses live_nesting_rel_eqs)
@@ -1644,7 +1644,7 @@
val thm =
Goal.prove_sorry lthy [] prems (HOLogic.mk_Trueprop concl)
(fn {context = ctxt, prems} =>
- mk_set_induct0_tac ctxt (map (certify ctxt'') Ps) prems dtor_set_inducts exhausts
+ mk_set_induct0_tac ctxt (map (Proof_Context.cterm_of ctxt'') Ps) prems dtor_set_inducts exhausts
set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses)
|> singleton (Proof_Context.export ctxt'' ctxt)
|> Thm.close_derivation;
@@ -1819,7 +1819,7 @@
val goalss = @{map 6} (map2 oooo mk_goal) cs cpss gcorecs ns kss discss;
- fun mk_case_split' cp = Drule.instantiate' [] [SOME (certify lthy cp)] @{thm case_split};
+ fun mk_case_split' cp = Drule.instantiate' [] [SOME (Proof_Context.cterm_of lthy cp)] @{thm case_split};
val case_splitss' = map (map mk_case_split') cpss;
@@ -1845,8 +1845,8 @@
let
val (domT, ranT) = dest_funT (fastype_of sel);
val arg_cong' =
- Drule.instantiate' (map (SOME o certifyT lthy) [domT, ranT])
- [NONE, NONE, SOME (certify lthy sel)] arg_cong
+ Drule.instantiate' (map (SOME o Proof_Context.ctyp_of lthy) [domT, ranT])
+ [NONE, NONE, SOME (Proof_Context.cterm_of lthy sel)] arg_cong
|> Thm.varifyT_global;
val sel_thm' = sel_thm RSN (2, trans);
in
@@ -2141,8 +2141,8 @@
(mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w)));
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_ctor_iff_dtor_tac ctxt (map (SOME o certifyT lthy) [ctr_absT, fpT])
- (certify lthy ctor) (certify lthy dtor) ctor_dtor dtor_ctor)
+ mk_ctor_iff_dtor_tac ctxt (map (SOME o Proof_Context.ctyp_of lthy) [ctr_absT, fpT])
+ (Proof_Context.cterm_of lthy ctor) (Proof_Context.cterm_of lthy dtor) ctor_dtor dtor_ctor)
|> Morphism.thm phi
|> Thm.close_derivation
end;
@@ -2233,7 +2233,7 @@
let val (Rs, Ss, goals, names_lthy) = mk_co_rec_transfer_goals lthy recs in
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
- mk_rec_transfer_tac ctxt nn ns (map (certify ctxt) Ss) (map (certify ctxt) Rs) xsssss
+ mk_rec_transfer_tac ctxt nn ns (map (Proof_Context.cterm_of ctxt) Ss) (map (Proof_Context.cterm_of ctxt) Rs) xsssss
rec_defs xtor_co_rec_transfers pre_rel_defs live_nesting_rel_eqs)
|> Conjunction.elim_balanced nn
|> Proof_Context.export names_lthy lthy
@@ -2385,7 +2385,7 @@
in
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
- mk_corec_transfer_tac ctxt (map (certify ctxt) Ss) (map (certify ctxt) Rs)
+ mk_corec_transfer_tac ctxt (map (Proof_Context.cterm_of ctxt) Ss) (map (Proof_Context.cterm_of ctxt) Rs)
type_definitions corec_defs xtor_co_rec_transfers pre_rel_defs
live_nesting_rel_eqs (flat pgss) pss qssss gssss)
|> Conjunction.elim_balanced (length goals)
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Mar 03 19:08:04 2015 +0100
@@ -97,7 +97,7 @@
val fs = Term.add_vars (prop_of thm) []
|> filter (fn (_, Type (@{type_name fun}, [_, T'])) => T' <> HOLogic.boolT | _ => false);
fun mk_cfp (f as (_, T)) =
- (certify ctxt (Var f), certify ctxt (mk_proj T (num_binder_types T) k));
+ (Proof_Context.cterm_of ctxt (Var f), Proof_Context.cterm_of ctxt (mk_proj T (num_binder_types T) k));
val cfps = map mk_cfp fs;
in
Drule.cterm_instantiate cfps thm
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Tue Mar 03 19:08:04 2015 +0100
@@ -191,7 +191,7 @@
case_fp fp (snd o Term.dest_comb) (snd o Term.dest_comb o fst o Term.dest_comb);
val raw_phis = map (extract o HOLogic.dest_Trueprop o Thm.concl_of) rel_xtor_co_inducts;
val thetas = AList.group (op =)
- (mutual_cliques ~~ map (apply2 (certify lthy)) (raw_phis ~~ pre_phis));
+ (mutual_cliques ~~ map (apply2 (Proof_Context.cterm_of lthy)) (raw_phis ~~ pre_phis));
in
map2 (Drule.cterm_instantiate o the o AList.lookup (op =) thetas)
mutual_cliques rel_xtor_co_inducts
@@ -214,7 +214,7 @@
fun mk_Grp_id P =
let val T = domain_type (fastype_of P);
in mk_Grp (HOLogic.Collect_const T $ P) (HOLogic.id_const T) end;
- val cts = map (SOME o certify lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps);
+ val cts = map (SOME o Proof_Context.cterm_of lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps);
fun mk_fp_type_copy_thms thm = map (curry op RS thm)
@{thms type_copy_Abs_o_Rep type_copy_vimage2p_Grp_Rep};
fun mk_type_copy_thms thm = map (curry op RS thm)
@@ -235,7 +235,7 @@
end
| Greatest_FP =>
let
- val cts = NONE :: map (SOME o certify lthy) (map HOLogic.eq_const As);
+ val cts = NONE :: map (SOME o Proof_Context.cterm_of lthy) (map HOLogic.eq_const As);
in
cterm_instantiate_pos cts xtor_rel_co_induct
|> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Tue Mar 03 19:08:04 2015 +0100
@@ -44,7 +44,7 @@
val else_branch = Var (("e", j), T);
val lam = Term.lambda cond (mk_If cond then_branch else_branch);
in
- cterm_instantiate_pos [SOME (certify ctxt lam)] thm
+ cterm_instantiate_pos [SOME (Proof_Context.cterm_of ctxt lam)] thm
end;
val transfer_rules =
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Tue Mar 03 19:08:04 2015 +0100
@@ -578,7 +578,7 @@
val n = Thm.nprems_of coind;
val m = Thm.nprems_of (hd rel_monos) - n;
fun mk_inst phi = (phi, mk_union (phi, HOLogic.eq_const (fst (dest_pred2T (fastype_of phi)))))
- |> apply2 (certify ctxt);
+ |> apply2 (Proof_Context.cterm_of ctxt);
val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map (mk_inst o Var);
fun mk_unfold rel_eq rel_mono =
let
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Tue Mar 03 19:08:04 2015 +0100
@@ -1080,7 +1080,7 @@
val goal = list_all_free (kl :: zs)
(Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
- val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
+ val cts = map (SOME o Proof_Context.cterm_of lthy) [Term.absfree nat' goal, nat];
val length_Lev =
Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
@@ -1115,8 +1115,8 @@
Library.foldr1 HOLogic.mk_conj
(map2 (mk_conjunct i z) ks zs_copy)) ks zs));
- val cTs = [SOME (certifyT lthy sum_sbdT)];
- val cts = map (SOME o certify lthy) [Term.absfree kl' goal, kl];
+ val cTs = [SOME (Proof_Context.ctyp_of lthy sum_sbdT)];
+ val cts = map (SOME o Proof_Context.cterm_of lthy) [Term.absfree kl' goal, kl];
val rv_last =
Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
@@ -1153,7 +1153,7 @@
val goal = list_all_free (kl :: zs @ zs_copy @ zs_copy2)
(Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
- val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
+ val cts = map (SOME o Proof_Context.cterm_of lthy) [Term.absfree nat' goal, nat];
val set_Lev =
Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
@@ -1192,7 +1192,7 @@
val goal = list_all_free (kl :: k :: zs @ zs_copy)
(Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
- val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
+ val cts = map (SOME o Proof_Context.cterm_of lthy) [Term.absfree nat' goal, nat];
val set_image_Lev =
Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
@@ -1867,7 +1867,7 @@
Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls
val ctss =
- map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls;
+ map (fn phi => map (SOME o Proof_Context.cterm_of lthy) [Term.absfree nat' phi, nat]) concls;
in
@{map 4} (fn goal => fn cts => fn col_0s => fn col_Sucs =>
Goal.prove_sorry lthy [] [] goal
@@ -1952,10 +1952,10 @@
maps (map (fn thm => thm RS @{thm subset_Collect_iff})) dtor_Jset_incl_thmss @
@{thms subset_Collect_iff[OF subset_refl]};
- val cTs = map (SOME o certifyT lthy) params';
+ val cTs = map (SOME o Proof_Context.ctyp_of lthy) params';
fun mk_induct_tinst phis jsets y y' =
@{map 4} (fn phi => fn jset => fn Jz => fn Jz' =>
- SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y',
+ SOME (Proof_Context.cterm_of lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y',
HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz))))))
phis jsets Jzs Jzs';
in
@@ -2024,7 +2024,7 @@
val goals = @{map 3} mk_goal fs colss colss';
val ctss =
- map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals;
+ map (fn phi => map (SOME o Proof_Context.cterm_of lthy) [Term.absfree nat' phi, nat]) goals;
val thms =
@{map 4} (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
@@ -2047,7 +2047,7 @@
val goals = map (mk_goal Jbds) colss;
- val ctss = map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat])
+ val ctss = map (fn phi => map (SOME o Proof_Context.cterm_of lthy) [Term.absfree nat' phi, nat])
(map (mk_goal (replicate n sbd)) colss);
val thms =
@@ -2064,7 +2064,7 @@
val map_cong0_thms =
let
- val cTs = map (SOME o certifyT lthy o
+ val cTs = map (SOME o Proof_Context.ctyp_of lthy o
Term.typ_subst_atomic (passiveAs ~~ passiveBs) o TFree) coinduct_params;
fun mk_prem z set f g y y' =
@@ -2086,7 +2086,7 @@
HOLogic.mk_exists (x, T, mk_coind_body sets z' z fmap gmap y y_copy)
|> Term.absfree y'_copy
|> Term.absfree y'
- |> certify lthy;
+ |> Proof_Context.cterm_of lthy;
val cphis = @{map 9} mk_cphi
Jsetss_by_bnf Jzs' Jzs fs_Jmaps fs_copy_Jmaps Jys' Jys Jys'_copy Jys_copy;
@@ -2189,9 +2189,9 @@
activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds;
fun mk_cts zs z's phis =
@{map 3} (fn z => fn z' => fn phi =>
- SOME (certify lthy (fold_rev (Term.absfree o Term.dest_Free) [z', z] phi)))
+ SOME (Proof_Context.cterm_of lthy (fold_rev (Term.absfree o Term.dest_Free) [z', z] phi)))
zs z's phis @
- map (SOME o certify lthy) (splice z's zs);
+ map (SOME o Proof_Context.cterm_of lthy) (splice z's zs);
val cts1 = mk_cts Jzs Jzs_copy coind1_phis;
val cts2 = mk_cts Jz's Jz's_copy coind2_phis;
@@ -2228,9 +2228,9 @@
Jphis abs fstABs sndABs;
val ctss = map2 (fn ab' => fn phis =>
map2 (fn z' => fn phi =>
- SOME (certify lthy (Term.absfree ab' (Term.absfree z' phi))))
+ SOME (Proof_Context.cterm_of lthy (Term.absfree ab' (Term.absfree z' phi))))
zip_zs' phis @
- map (SOME o certify lthy) zip_zs)
+ map (SOME o Proof_Context.cterm_of lthy) zip_zs)
abs' helper_ind_phiss;
fun mk_helper_ind_concl ab' z ind_phi set =
mk_Ball (set $ z) (Term.absfree ab' ind_phi);
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Tue Mar 03 19:08:04 2015 +0100
@@ -43,7 +43,7 @@
val fs = Term.add_vars (prop_of thm) [] |> filter (can dest_funT o snd);
fun find s = find_index (curry (op =) s) frees;
fun mk_cfp (f as ((s, _), T)) =
- (certify ctxt (Var f), certify ctxt (mk_proj T num_frees (find s)));
+ (Proof_Context.cterm_of ctxt (Var f), Proof_Context.cterm_of ctxt (mk_proj T num_frees (find s)));
val cfps = map mk_cfp fs;
in
Drule.cterm_instantiate cfps thm
@@ -154,7 +154,7 @@
let
val s = Name.uu;
val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
- val split' = Drule.instantiate' [] [SOME (certify ctxt eq)] split;
+ val split' = Drule.instantiate' [] [SOME (Proof_Context.cterm_of ctxt eq)] split;
in
Thm.generalize ([], [s]) (Thm.maxidx_of split' + 1) split'
end
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Tue Mar 03 19:08:04 2015 +0100
@@ -607,8 +607,8 @@
fun mk_card_conjunct min_alg = mk_ordLeq (mk_card_of min_alg) Asuc_bd;
val card_conjunction = Library.foldr1 HOLogic.mk_conj (map mk_card_conjunct min_algss);
- val card_cT = certifyT lthy suc_bdT;
- val card_ct = certify lthy (Term.absfree idx' card_conjunction);
+ val card_cT = Proof_Context.ctyp_of lthy suc_bdT;
+ val card_ct = Proof_Context.cterm_of lthy (Term.absfree idx' card_conjunction);
val card_of =
Goal.prove_sorry lthy [] []
@@ -622,8 +622,8 @@
val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_leq min_algss Bs);
- val least_cT = certifyT lthy suc_bdT;
- val least_ct = certify lthy (Term.absfree idx' least_conjunction);
+ val least_cT = Proof_Context.ctyp_of lthy suc_bdT;
+ val least_ct = Proof_Context.cterm_of lthy (Term.absfree idx' least_conjunction);
val least =
(Goal.prove_sorry lthy [] []
@@ -779,7 +779,7 @@
val car_inits = map (mk_min_alg str_inits) ks;
- val alg_init_thm = cterm_instantiate_pos (map (SOME o certify lthy) str_inits) alg_min_alg_thm;
+ val alg_init_thm = cterm_instantiate_pos (map (SOME o Proof_Context.cterm_of lthy) str_inits) alg_min_alg_thm;
val alg_select_thm = Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (mk_Ball II
@@ -812,7 +812,7 @@
fun mk_fun_eq f g x = HOLogic.mk_eq (f $ x, g $ x);
val unique = HOLogic.mk_Trueprop
(Library.foldr1 HOLogic.mk_conj (@{map 3} mk_fun_eq init_fs init_fs_copy init_xs));
- val cts = map (certify lthy) ss;
+ val cts = map (Proof_Context.cterm_of lthy) ss;
val unique_mor =
Goal.prove_sorry lthy [] [] (Logic.list_implies (prems @ mor_prems, unique))
(K (mk_init_unique_mor_tac cts m alg_def alg_init_thm least_min_alg_thms
@@ -946,7 +946,7 @@
|> Thm.close_derivation;
fun mk_ct initFT str abs = Term.absdummy initFT (abs $ (str $ Bound 0))
- val cts = @{map 3} (certify lthy ooo mk_ct) init_FTs str_inits Abs_Ts;
+ val cts = @{map 3} (Proof_Context.cterm_of lthy ooo mk_ct) init_FTs str_inits Abs_Ts;
val mor_Abs =
Goal.prove_sorry lthy [] []
@@ -1020,8 +1020,8 @@
val mor_fold_thm =
let
val mor_cong = mor_cong_thm OF (map (mk_nth_conv n) ks);
- val cT = certifyT lthy foldT;
- val ct = certify lthy fold_fun
+ val cT = Proof_Context.ctyp_of lthy foldT;
+ val ct = Proof_Context.cterm_of lthy fold_fun
in
Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_fold Ts ss) ks)))
@@ -1244,7 +1244,7 @@
rev (Term.add_tfrees goal []))
end;
- val cTs = map (SOME o certifyT lthy o TFree) induct_params;
+ val cTs = map (SOME o Proof_Context.ctyp_of lthy o TFree) induct_params;
val weak_ctor_induct_thms =
let fun insts i = (replicate (i - 1) TrueI) @ (asm_rl :: replicate (n - i) TrueI);
@@ -1276,7 +1276,7 @@
(@{map 3} mk_concl phi2s Izs1 Izs2));
fun mk_t phi (z1, z1') (z2, z2') =
Term.absfree z1' (HOLogic.mk_all (fst z2', snd z2', phi $ z1 $ z2));
- val cts = @{map 3} (SOME o certify lthy ooo mk_t) phi2s (Izs1 ~~ Izs1') (Izs2 ~~ Izs2');
+ val cts = @{map 3} (SOME o Proof_Context.cterm_of lthy ooo mk_t) phi2s (Izs1 ~~ Izs1') (Izs2 ~~ Izs2');
val goal = Logic.list_implies (prems, concl);
in
(Goal.prove_sorry lthy [] [] goal
@@ -1552,7 +1552,7 @@
val timer = time (timer "set functions for the new datatypes");
- val cxs = map (SOME o certify lthy) Izs;
+ val cxs = map (SOME o Proof_Context.cterm_of lthy) Izs;
val Isetss_by_range' =
map (map (Term.subst_atomic_types (passiveAs ~~ passiveBs))) Isetss_by_range;
@@ -1561,10 +1561,10 @@
fun mk_set_map0 f map z set set' =
HOLogic.mk_eq (mk_image f $ (set $ z), set' $ (map $ z));
- fun mk_cphi f map z set set' = certify lthy
+ fun mk_cphi f map z set set' = Proof_Context.cterm_of lthy
(Term.absfree (dest_Free z) (mk_set_map0 f map z set set'));
- val csetss = map (map (certify lthy)) Isetss_by_range';
+ val csetss = map (map (Proof_Context.cterm_of lthy)) Isetss_by_range';
val cphiss = @{map 3} (fn f => fn sets => fn sets' =>
(@{map 4} (mk_cphi f) fs_Imaps Izs sets sets')) fs Isetss_by_range Isetss_by_range';
@@ -1594,7 +1594,7 @@
let
fun mk_set_bd z bd set = mk_ordLeq (mk_card_of (set $ z)) bd;
- fun mk_cphi z set = certify lthy (Term.absfree (dest_Free z) (mk_set_bd z sbd0 set));
+ fun mk_cphi z set = Proof_Context.cterm_of lthy (Term.absfree (dest_Free z) (mk_set_bd z sbd0 set));
val cphiss = map (map2 mk_cphi Izs) Isetss_by_range;
@@ -1630,7 +1630,7 @@
HOLogic.mk_eq (fmap $ z, gmap $ z));
fun mk_cphi sets z fmap gmap =
- certify lthy (Term.absfree (dest_Free z) (mk_map_cong0 sets z fmap gmap));
+ Proof_Context.cterm_of lthy (Term.absfree (dest_Free z) (mk_map_cong0 sets z fmap gmap));
val cphis = @{map 4} mk_cphi Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps;
@@ -1691,9 +1691,9 @@
Irelpsi12 $ Iz1 $ Iz2);
val goals = @{map 5} mk_le_Irel_OO Irelpsi1s Irelpsi2s Irelpsi12s Izs1 Izs2;
- val cTs = map (SOME o certifyT lthy o TFree) induct2_params;
- val cxs = map (SOME o certify lthy) (splice Izs1 Izs2);
- fun mk_cphi z1 z2 goal = SOME (certify lthy (Term.absfree z1 (Term.absfree z2 goal)));
+ val cTs = map (SOME o Proof_Context.ctyp_of lthy o TFree) induct2_params;
+ val cxs = map (SOME o Proof_Context.cterm_of lthy) (splice Izs1 Izs2);
+ fun mk_cphi z1 z2 goal = SOME (Proof_Context.cterm_of lthy (Term.absfree z1 (Term.absfree z2 goal)));
val cphis = @{map 3} mk_cphi Izs1' Izs2' goals;
val induct = Drule.instantiate' cTs (cphis @ cxs) ctor_induct2_thm;
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Mar 03 19:08:04 2015 +0100
@@ -273,7 +273,7 @@
HOLogic.mk_Trueprop (BNF_LFP_Util.mk_not_eq (list_comb (size, xs)) HOLogic.zero);
val thm =
Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
- mk_size_neq ctxt (map (certify lthy2) xs)
+ mk_size_neq ctxt (map (Proof_Context.cterm_of lthy2) xs)
(#exhaust (#ctr_sugar (#fp_ctr_sugar fp_sugar))) size_thms)
|> single
|> Proof_Context.export names_lthy2 lthy2
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Mar 03 19:08:04 2015 +0100
@@ -679,10 +679,10 @@
let
val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat;
- val rho_As = map (apply2 (certifyT lthy)) (map Logic.varifyT_global As ~~ As);
+ val rho_As = map (apply2 (Proof_Context.ctyp_of lthy)) (map Logic.varifyT_global As ~~ As);
fun inst_thm t thm =
- Drule.instantiate' [] [SOME (certify lthy t)]
+ Drule.instantiate' [] [SOME (Proof_Context.cterm_of lthy t)]
(Thm.instantiate (rho_As, []) (Drule.zero_var_indexes thm));
val uexhaust_thm = inst_thm u exhaust_thm;
@@ -997,7 +997,7 @@
mk_Trueprop_eq (udisc, list_comb (casexBool, mk_case_args n) $ u)) udiscs;
in
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
- (fn {context = ctxt, ...} => mk_disc_eq_case_tac ctxt (certify ctxt u)
+ (fn {context = ctxt, ...} => mk_disc_eq_case_tac ctxt (Proof_Context.cterm_of ctxt u)
exhaust_thm (flat nontriv_disc_thmss) distinct_thms case_thms)
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
@@ -1020,7 +1020,7 @@
val goal = mk_Trueprop_eq (h $ ufcase, list_comb (casexC, args) $ u);
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_case_distrib_tac ctxt (certify ctxt u) exhaust_thm case_thms)
+ mk_case_distrib_tac ctxt (Proof_Context.cterm_of ctxt u) exhaust_thm case_thms)
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
end;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Tue Mar 03 19:08:04 2015 +0100
@@ -62,9 +62,6 @@
val cterm_instantiate_pos: cterm option list -> thm -> thm
val unfold_thms: Proof.context -> thm list -> thm -> thm
- val certifyT: Proof.context -> typ -> ctyp
- val certify: Proof.context -> term -> cterm
-
val name_noted_thms: string -> string -> (string * thm list) list -> (string * thm list) list
val substitute_noted_thm: (string * thm list) list -> morphism
@@ -226,10 +223,6 @@
fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
-(*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
-val certifyT = Thm.ctyp_of o Proof_Context.theory_of;
-val certify = Thm.cterm_of o Proof_Context.theory_of;
-
fun name_noted_thms _ _ [] = []
| name_noted_thms qualifier base ((local_name, thms) :: noted) =
if Long_Name.base_name local_name = base then
--- a/src/HOL/Tools/Function/function_context_tree.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/Function/function_context_tree.ML Tue Mar 03 19:08:04 2015 +0100
@@ -149,7 +149,7 @@
val (r, dep, branches) = find_cong_rule ctxt fvar h congs_deps t
fun subtree (ctxt', fixes, assumes, st) =
((fixes,
- map (Thm.assume o cterm_of (Proof_Context.theory_of ctxt)) assumes),
+ map (Thm.assume o Proof_Context.cterm_of ctxt) assumes),
mk_tree' ctxt' st)
in
Cong (r, dep, map subtree branches)
--- a/src/HOL/Tools/Function/function_core.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/Function/function_core.ML Tue Mar 03 19:08:04 2015 +0100
@@ -183,7 +183,7 @@
val Globals {h, ...} = globals
val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
- val cert = Thm.cterm_of (Proof_Context.theory_of ctxt)
+ val cert = Proof_Context.cterm_of ctxt
(* Instantiate the GIntro thm with "f" and import into the clause context. *)
val lGI = GIntro_thm
@@ -453,7 +453,7 @@
[] (* no special monos *)
||> Local_Theory.restore_naming lthy
- val cert = cterm_of (Proof_Context.theory_of lthy)
+ val cert = Proof_Context.cterm_of lthy
fun requantify orig_intro thm =
let
val (qs, t) = dest_all_all orig_intro
@@ -871,7 +871,7 @@
val newthy = Proof_Context.theory_of lthy
val clauses = map (transfer_clause_ctx newthy) clauses
- val cert = cterm_of (Proof_Context.theory_of lthy)
+ val cert = Proof_Context.cterm_of lthy
val xclauses = PROFILE "xclauses"
(@{map 7} (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
--- a/src/HOL/Tools/Function/induction_schema.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Tue Mar 03 19:08:04 2015 +0100
@@ -354,7 +354,7 @@
val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt'
val R = Free (Rn, mk_relT ST)
val x = Free (xn, ST)
- val cert = cterm_of (Proof_Context.theory_of ctxt)
+ val cert = Proof_Context.cterm_of ctxt
val ineqss = mk_ineqs R scheme |> map (map (apply2 (Thm.assume o cert)))
val complete =
--- a/src/HOL/Tools/Function/measure_functions.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/Function/measure_functions.ML Tue Mar 03 19:08:04 2015 +0100
@@ -20,7 +20,7 @@
fun find_measures ctxt T =
DEPTH_SOLVE (resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems measure_function})) 1)
(HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT)))
- |> cterm_of (Proof_Context.theory_of ctxt) |> Goal.init)
+ |> Proof_Context.cterm_of ctxt |> Goal.init)
|> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
|> Seq.list_of
--- a/src/HOL/Tools/Function/mutual.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/Function/mutual.ML Tue Mar 03 19:08:04 2015 +0100
@@ -209,7 +209,7 @@
fun mutual_induct_rules ctxt induct all_f_defs (Mutual {n, ST, parts, ...}) =
let
- val cert = cterm_of (Proof_Context.theory_of ctxt)
+ val cert = Proof_Context.cterm_of ctxt
val newPs =
map2 (fn Pname => fn MutualPart {cargTs, ...} =>
Free (Pname, cargTs ---> HOLogic.boolT))
@@ -259,7 +259,7 @@
val argsT = fastype_of (HOLogic.mk_tuple arg_vars)
val (args, name_ctxt) = mk_var "x" argsT name_ctxt
- val cert = cterm_of (Proof_Context.theory_of ctxt)
+ val cert = Proof_Context.cterm_of ctxt
val P = mk_var "P" @{typ "bool"} name_ctxt |> fst |> cert
val sumtree_inj = Sum_Tree.mk_inj ST n i args
--- a/src/HOL/Tools/Function/partial_function.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML Tue Mar 03 19:08:04 2015 +0100
@@ -168,7 +168,7 @@
curry induction predicate *)
fun specialize_fixp_induct ctxt args fT fT_uc F curry uncurry mono_thm f_def rule =
let
- val cert = Thm.cterm_of (Proof_Context.theory_of ctxt)
+ val cert = Proof_Context.cterm_of ctxt
val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
val P_inst = Abs ("f", fT_uc, Free (P, fT --> HOLogic.boolT) $ (curry $ Bound 0))
in
@@ -187,7 +187,7 @@
fun mk_curried_induct args ctxt inst_rule =
let
- val cert = Thm.cterm_of (Proof_Context.theory_of ctxt)
+ val cert = Proof_Context.cterm_of ctxt
val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
val split_paired_all_conv =
@@ -234,7 +234,7 @@
val ((f_binding, fT), mixfix) = the_single fixes;
val fname = Binding.name_of f_binding;
- val cert = cterm_of (Proof_Context.theory_of lthy);
+ val cert = Proof_Context.cterm_of lthy;
val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop plain_eqn);
val (head, args) = strip_comb lhs;
val argnames = map (fst o dest_Free) args;
--- a/src/HOL/Tools/Function/pat_completeness.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/Function/pat_completeness.ML Tue Mar 03 19:08:04 2015 +0100
@@ -88,8 +88,8 @@
then o_alg ctxt P idx vs
(map (fn (pv :: pats, thm) =>
(pats, refl RS
- (inst_free (cterm_of (Proof_Context.theory_of ctxt) pv)
- (cterm_of (Proof_Context.theory_of ctxt) v) thm))) pts)
+ (inst_free (Proof_Context.cterm_of ctxt pv)
+ (Proof_Context.cterm_of ctxt v) thm))) pts)
else (* Cons case *)
let
val thy = Proof_Context.theory_of ctxt
--- a/src/HOL/Tools/Function/relation.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/Function/relation.ML Tue Mar 03 19:08:04 2015 +0100
@@ -33,7 +33,7 @@
case Term.add_vars (prop_of st) [] of
[v as (_, T)] =>
let
- val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
+ val cert = Proof_Context.cterm_of ctxt;
val rel' = singleton (Variable.polymorphic ctxt) rel
|> map_types Type_Infer.paramify_vars
|> Type.constraint T
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Tue Mar 03 19:08:04 2015 +0100
@@ -23,7 +23,7 @@
fun get_lhs thm = thm |> concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst
val vars = get_lhs rel_Grp |> strip_comb |> snd |> map_filter (try (strip_comb #> snd #> hd))
val UNIVs = map (fn var => HOLogic.mk_UNIV (var |> dest_Var |> snd |> dest_Type |> snd |> hd)) vars
- val inst = map2 (curry (apply2 (certify ctxt))) vars UNIVs
+ val inst = map2 (curry (apply2 (Proof_Context.cterm_of ctxt))) vars UNIVs
val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize ([], inst)
|> Local_Defs.unfold ctxt @{thms subset_UNIV[THEN eqTrueI] UNIV_def[symmetric] simp_thms(21)}
|> (fn thm => thm RS sym)
--- a/src/HOL/Tools/Lifting/lifting_def.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Tue Mar 03 19:08:04 2015 +0100
@@ -495,7 +495,7 @@
in
fun mk_readable_rsp_thm_eq tm lthy =
let
- val ctm = cterm_of (Proof_Context.theory_of lthy) tm
+ val ctm = Proof_Context.cterm_of lthy tm
fun assms_rewr_conv tactic rule ct =
let
@@ -620,7 +620,7 @@
val cr_to_pcr_conv = HOLogic.Trueprop_conv (Conv.fun2_conv
(Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy)))
val (prsp_tm, rsp_prsp_eq) = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs)
- |> cterm_of (Proof_Context.theory_of lthy)
+ |> Proof_Context.cterm_of lthy
|> cr_to_pcr_conv
|> ` concl_of
|>> Logic.dest_equals
--- a/src/HOL/Tools/Meson/meson.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/Meson/meson.ML Tue Mar 03 19:08:04 2015 +0100
@@ -352,7 +352,7 @@
in
fun freeze_spec th ctxt =
let
- val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
+ val cert = Proof_Context.cterm_of ctxt;
val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt;
val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec;
in (th RS spec', ctxt') end
--- a/src/HOL/Tools/Qelim/cooper.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Tue Mar 03 19:08:04 2015 +0100
@@ -694,7 +694,7 @@
val (_, oracle) = Context.>>> (Context.map_theory_result
(Thm.add_oracle (@{binding cooper},
(fn (ctxt, t) =>
- (Thm.cterm_of (Proof_Context.theory_of ctxt) o Logic.mk_equals o apply2 HOLogic.mk_Trueprop)
+ (Proof_Context.cterm_of ctxt o Logic.mk_equals o apply2 HOLogic.mk_Trueprop)
(t, procedure t)))));
val comp_ss =
--- a/src/HOL/Tools/Quotient/quotient_def.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Tue Mar 03 19:08:04 2015 +0100
@@ -91,7 +91,7 @@
fun mk_readable_rsp_thm_eq tm lthy =
let
- val ctm = cterm_of (Proof_Context.theory_of lthy) tm
+ val ctm = Proof_Context.cterm_of lthy tm
fun norm_fun_eq ctm =
let
--- a/src/HOL/Tools/SMT/smt_util.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/SMT/smt_util.ML Tue Mar 03 19:08:04 2015 +0100
@@ -45,7 +45,6 @@
val instT': cterm -> ctyp * cterm -> cterm
(*certified terms*)
- val certify: Proof.context -> term -> cterm
val typ_of: cterm -> typ
val dest_cabs: cterm -> Proof.context -> cterm * Proof.context
val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context
@@ -180,8 +179,6 @@
(* certified terms *)
-fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt)
-
fun typ_of ct = #T (Thm.rep_cterm ct)
fun dest_cabs ct ctxt =
--- a/src/HOL/Tools/SMT/z3_replay.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/SMT/z3_replay.ML Tue Mar 03 19:08:04 2015 +0100
@@ -23,7 +23,7 @@
val maxidx = Thm.maxidx_of thm + 1
val vs = params_of (Thm.prop_of thm)
val vars = map_index (fn (i, (n, T)) => Var ((n, i + maxidx), T)) vs
- in Drule.forall_elim_list (map (SMT_Util.certify ctxt) vars) thm end
+ in Drule.forall_elim_list (map (Proof_Context.cterm_of ctxt) vars) thm end
fun add_paramTs names t =
fold2 (fn n => fn (_, T) => AList.update (op =) (n, T)) names (params_of t)
@@ -31,7 +31,7 @@
fun new_fixes ctxt nTs =
let
val (ns, ctxt') = Variable.variant_fixes (replicate (length nTs) "") ctxt
- fun mk (n, T) n' = (n, SMT_Util.certify ctxt' (Free (n', T)))
+ fun mk (n, T) n' = (n, Proof_Context.cterm_of ctxt' (Free (n', T)))
in (ctxt', Symtab.make (map2 mk nTs ns)) end
fun forall_elim_term ct (Const (@{const_name Pure.all}, _) $ (a as Abs _)) =
@@ -60,7 +60,7 @@
if Z3_Proof.is_assumption rule then
(case Inttab.lookup assumed id of
SOME (_, thm) => thm
- | NONE => Thm.assume (SMT_Util.certify ctxt concl))
+ | NONE => Thm.assume (Proof_Context.cterm_of ctxt concl))
else
under_fixes (Z3_Replay_Methods.method_for rule) ctxt
(if is_fix_step then (map snd nthms, []) else ([], nthms)) fixes concl
@@ -123,7 +123,7 @@
(cx as ((iidths, thms), (ctxt, ptab))) =
if Z3_Proof.is_assumption rule andalso rule <> Z3_Proof.Hypothesis then
let
- val ct = SMT_Util.certify ctxt concl
+ val ct = Proof_Context.cterm_of ctxt concl
val thm1 = Thm.trivial ct |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))
val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1
in
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Tue Mar 03 19:08:04 2015 +0100
@@ -88,7 +88,7 @@
fun dest_thm thm = dest_prop (Thm.concl_of thm)
-fun certify_prop ctxt t = SMT_Util.certify ctxt (as_prop t)
+fun certify_prop ctxt t = Proof_Context.cterm_of ctxt (as_prop t)
fun try_provers ctxt rule [] thms t = replay_rule_error ctxt rule thms t
| try_provers ctxt rule ((name, prover) :: named_provers) thms t =
@@ -108,13 +108,13 @@
fun match_instantiateT ctxt t thm =
if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then
- let val certT = Thm.ctyp_of (Proof_Context.theory_of ctxt)
+ let val certT = Proof_Context.ctyp_of ctxt
in Thm.instantiate (gen_certify_inst fst TVar certT ctxt thm t, []) thm end
else thm
fun match_instantiate ctxt t thm =
let
- val cert = SMT_Util.certify ctxt
+ val cert = Proof_Context.cterm_of ctxt
val thm' = match_instantiateT ctxt t thm
in Thm.instantiate ([], gen_certify_inst snd Var cert ctxt thm' t) thm' end
@@ -402,7 +402,7 @@
end
fun forall_intr ctxt t thm =
- let val ct = Thm.cterm_of (Proof_Context.theory_of ctxt) t
+ let val ct = Proof_Context.cterm_of ctxt t
in Thm.forall_intr ct thm COMP_INCR @{thm iff_allI} end
in
--- a/src/HOL/Tools/TFL/post.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/TFL/post.ML Tue Mar 03 19:08:04 2015 +0100
@@ -174,7 +174,7 @@
(warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
in
fun derive_init_eqs ctxt rules eqs =
- map (Thm.trivial o Thm.cterm_of (Proof_Context.theory_of ctxt) o HOLogic.mk_Trueprop) eqs
+ map (Thm.trivial o Proof_Context.cterm_of ctxt o HOLogic.mk_Trueprop) eqs
|> map_index (fn (i, e) => solve_eq ctxt (e, (get_related_thms i rules), i))
|> flat;
end;
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Tue Mar 03 19:08:04 2015 +0100
@@ -343,8 +343,8 @@
val predTs = map mk_pred1T As
val (preds, lthy) = mk_Frees "P" predTs lthy
val args = map mk_eq_onp preds
- val cTs = map (SOME o certifyT lthy) (maps (replicate 2) As)
- val cts = map (SOME o certify lthy) args
+ val cTs = map (SOME o Proof_Context.ctyp_of lthy) (maps (replicate 2) As)
+ val cts = map (SOME o Proof_Context.cterm_of lthy) args
fun get_rhs thm = thm |> concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
fun is_eqn thm = can get_rhs thm
fun rel2pred_massage thm =
--- a/src/HOL/Tools/code_evaluation.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/code_evaluation.ML Tue Mar 03 19:08:04 2015 +0100
@@ -204,7 +204,7 @@
fun certify_eval ctxt value conv ct =
let
- val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
+ val cert = Proof_Context.cterm_of ctxt;
val t = Thm.term_of ct;
val T = fastype_of t;
val mk_eq = Thm.mk_binop (cert (Const (@{const_name Pure.eq}, T --> T --> propT)));
--- a/src/HOL/Tools/coinduction.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/coinduction.ML Tue Mar 03 19:08:04 2015 +0100
@@ -79,7 +79,7 @@
|> Ctr_Sugar_Util.list_exists_free vars
|> Term.map_abs_vars (Variable.revert_fixed ctxt)
|> fold_rev Term.absfree (names ~~ Ts)
- |> Ctr_Sugar_Util.certify ctxt;
+ |> Proof_Context.cterm_of ctxt;
val thm = Ctr_Sugar_Util.cterm_instantiate_pos [SOME phi] raw_thm;
val e = length eqs;
val p = length prems;
@@ -88,7 +88,7 @@
EVERY' (map (fn var =>
resolve_tac ctxt
[Ctr_Sugar_Util.cterm_instantiate_pos
- [NONE, SOME (Ctr_Sugar_Util.certify ctxt var)] exI]) vars),
+ [NONE, SOME (Proof_Context.cterm_of ctxt var)] exI]) vars),
if p = 0 then Ctr_Sugar_Util.CONJ_WRAP' (K (resolve_tac ctxt [refl])) eqs
else
REPEAT_DETERM_N e o (resolve_tac ctxt [conjI] THEN' resolve_tac ctxt [refl]) THEN'
--- a/src/HOL/Tools/inductive.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/inductive.ML Tue Mar 03 19:08:04 2015 +0100
@@ -849,7 +849,7 @@
||> is_auxiliary ? Local_Theory.restore_naming lthy;
val fp_def' =
Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def])
- (cterm_of (Proof_Context.theory_of lthy') (list_comb (rec_const, params)));
+ (Proof_Context.cterm_of lthy' (list_comb (rec_const, params)));
val specs =
if length cs < 2 then []
else
--- a/src/HOL/Tools/legacy_transfer.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/legacy_transfer.ML Tue Mar 03 19:08:04 2015 +0100
@@ -59,9 +59,8 @@
fun get_by_direction context (a, D) =
let
val ctxt = Context.proof_of context;
- val certify = Thm.cterm_of (Context.theory_of context);
- val a0 = certify a;
- val D0 = certify D;
+ val a0 = Proof_Context.cterm_of ctxt a;
+ val D0 = Proof_Context.cterm_of ctxt D;
fun eq_direction ((a, D), thm') =
let
val (a', D') = direction_of thm';
@@ -117,12 +116,11 @@
|> Variable.declare_thm thm
|> Variable.declare_term (term_of a)
|> Variable.declare_term (term_of D);
- val certify = Thm.cterm_of (Proof_Context.theory_of ctxt3);
val vars = filter (fn ((v, _), T) => Type.could_unify (T, aT) andalso
not (member (op =) leave v)) (Term.add_vars (Thm.prop_of thm) []);
- val c_vars = map (certify o Var) vars;
+ val c_vars = map (Proof_Context.cterm_of ctxt3 o Var) vars;
val (vs', ctxt4) = Variable.variant_fixes (map (fst o fst) vars) ctxt3;
- val c_vars' = map (certify o (fn v => Free (v, bT))) vs';
+ val c_vars' = map (Proof_Context.cterm_of ctxt3 o (fn v => Free (v, bT))) vs';
val c_exprs' = map (Thm.apply a) c_vars';
(* transfer *)
--- a/src/HOL/Tools/reification.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/reification.ML Tue Mar 03 19:08:04 2015 +0100
@@ -27,7 +27,7 @@
let
val ct = case some_t
of NONE => Thm.dest_arg concl
- | SOME t => Thm.cterm_of (Proof_Context.theory_of ctxt) t
+ | SOME t => Proof_Context.cterm_of ctxt t
val thm = conv ct;
in
if Thm.is_reflexive thm then no_tac
@@ -48,7 +48,7 @@
let
val Const (fN, _) = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
|> fst |> strip_comb |> fst;
- val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
+ val cert = Proof_Context.cterm_of ctxt;
val ((_, [th']), ctxt') = Variable.import true [th] ctxt;
val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'));
fun add_fterms (t as t1 $ t2) =
@@ -261,7 +261,7 @@
|> fst)) eqs [];
val tys = fold_rev (fn f => fold (insert (op =)) (f |> fastype_of |> binder_types |> tl)) fs [];
val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt;
- val cert = cterm_of (Proof_Context.theory_of ctxt');
+ val cert = Proof_Context.cterm_of ctxt';
val subst =
the o AList.lookup (op =) (map2 (fn T => fn v => (T, cert (Free (v, T)))) tys vs);
fun prep_eq eq =
@@ -285,7 +285,7 @@
| is_list_var _ = false;
val vars = th |> prop_of |> Logic.dest_equals |> snd
|> strip_comb |> snd |> filter is_list_var;
- val cert = cterm_of (Proof_Context.theory_of ctxt);
+ val cert = Proof_Context.cterm_of ctxt;
val vs = map (fn v as Var (_, T) =>
(v, the (AList.lookup Type.could_unify bds' T) |> snd |> HOLogic.mk_list (dest_listT T))) vars;
val th' = Drule.instantiate_normalize ([], (map o apply2) cert vs) th;
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Tue Mar 03 19:08:04 2015 +0100
@@ -468,7 +468,7 @@
fun conv ctxt t =
let
val ([t'], ctxt') = Variable.import_terms true [t] (Variable.declare_term t ctxt)
- val ct = cterm_of (Proof_Context.theory_of ctxt') t'
+ val ct = Proof_Context.cterm_of ctxt' t'
fun unfold_conv thms =
Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
(empty_simpset ctxt' addsimps thms)
@@ -495,11 +495,10 @@
fun instantiate_arg_cong ctxt pred =
let
- val certify = cterm_of (Proof_Context.theory_of ctxt)
val arg_cong = Thm.incr_indexes (maxidx_of_term pred + 1) @{thm arg_cong}
val f $ _ = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (concl_of arg_cong)))
in
- cterm_instantiate [(certify f, certify pred)] arg_cong
+ cterm_instantiate [(Proof_Context.cterm_of ctxt f, Proof_Context.cterm_of ctxt pred)] arg_cong
end;
fun simproc ctxt redex =