# HG changeset patch # User traytel # Date 1425406084 -3600 # Node ID cbc38731d42f18d9b645a1bde6ac60f3ab3e5752 # Parent d8fff0b94c53ea0db5f97025af5a2a9b99b791c2 eliminated some clones of Proof_Context.cterm_of diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Decision_Procs/Approximation.thy --- 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), diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Decision_Procs/Ferrack.thy --- 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; *} diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- 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 diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Decision_Procs/approximation.ML --- 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 diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Library/Old_SMT/old_smt_utils.ML --- 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) diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML --- 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) diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Library/simps_case_conv.ML --- 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 diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Multivariate_Analysis/normarith.ML --- 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' = diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Nominal/nominal_induct.ML --- 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; diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Nominal/nominal_primrec.ML --- 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 diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/BNF/bnf_def.ML --- 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}) diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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) diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- 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 diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/BNF/bnf_fp_n2m.ML --- 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]} @ diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML --- 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 = diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/BNF/bnf_fp_util.ML --- 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 diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/BNF/bnf_gfp.ML --- 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); diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML --- 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 diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/BNF/bnf_lfp.ML --- 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; diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/BNF/bnf_lfp_size.ML --- 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 diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- 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; diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML --- 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 diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/Function/function_context_tree.ML --- 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) diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/Function/function_core.ML --- 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 diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/Function/induction_schema.ML --- 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 = diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/Function/measure_functions.ML --- 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 diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/Function/mutual.ML --- 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 diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/Function/partial_function.ML --- 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; diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/Function/pat_completeness.ML --- 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 diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/Function/relation.ML --- 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 diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/Lifting/lifting_bnf.ML --- 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) diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/Lifting/lifting_def.ML --- 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 diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/Meson/meson.ML --- 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 diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/Qelim/cooper.ML --- 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 = diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/Quotient/quotient_def.ML --- 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 diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/SMT/smt_util.ML --- 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 = diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/SMT/z3_replay.ML --- 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 diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/SMT/z3_replay_methods.ML --- 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 diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/TFL/post.ML --- 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; diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/Transfer/transfer_bnf.ML --- 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 = diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/code_evaluation.ML --- 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))); diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/coinduction.ML --- 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' diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/inductive.ML --- 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 diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/legacy_transfer.ML --- 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 *) diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/reification.ML --- 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; diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/set_comprehension_pointfree.ML --- 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 =