eliminated some clones of Proof_Context.cterm_of
authortraytel
Tue Mar 03 19:08:04 2015 +0100 (2015-03-03)
changeset 59580cbc38731d42f
parent 59579 d8fff0b94c53
child 59581 09722854b8f4
child 59582 0fbed69ff081
child 59587 8ea7b22525cb
eliminated some clones of Proof_Context.cterm_of
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/approximation.ML
src/HOL/Library/Old_SMT/old_smt_utils.ML
src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML
src/HOL/Library/simps_case_conv.ML
src/HOL/Multivariate_Analysis/normarith.ML
src/HOL/Nominal/nominal_induct.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Tools/BNF/bnf_lfp_size.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
src/HOL/Tools/Function/function_context_tree.ML
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Function/measure_functions.ML
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Function/partial_function.ML
src/HOL/Tools/Function/pat_completeness.ML
src/HOL/Tools/Function/relation.ML
src/HOL/Tools/Lifting/lifting_bnf.ML
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/SMT/smt_util.ML
src/HOL/Tools/SMT/z3_replay.ML
src/HOL/Tools/SMT/z3_replay_methods.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/Transfer/transfer_bnf.ML
src/HOL/Tools/code_evaluation.ML
src/HOL/Tools/coinduction.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/legacy_transfer.ML
src/HOL/Tools/reification.ML
src/HOL/Tools/set_comprehension_pointfree.ML
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Tue Mar 03 17:20:51 2015 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Mar 03 19:08:04 2015 +0100
     1.3 @@ -3641,16 +3641,16 @@
     1.4                 |> HOLogic.dest_list
     1.5        val p = prec
     1.6                |> HOLogic.mk_number @{typ nat}
     1.7 -              |> Thm.cterm_of (Proof_Context.theory_of ctxt)
     1.8 +              |> Proof_Context.cterm_of ctxt
     1.9      in case taylor
    1.10      of NONE => let
    1.11           val n = vs |> length
    1.12                   |> HOLogic.mk_number @{typ nat}
    1.13 -                 |> Thm.cterm_of (Proof_Context.theory_of ctxt)
    1.14 +                 |> Proof_Context.cterm_of ctxt
    1.15           val s = vs
    1.16                   |> map lookup_splitting
    1.17                   |> HOLogic.mk_list @{typ nat}
    1.18 -                 |> Thm.cterm_of (Proof_Context.theory_of ctxt)
    1.19 +                 |> Proof_Context.cterm_of ctxt
    1.20         in
    1.21           (rtac (Thm.instantiate ([], [(@{cpat "?n::nat"}, n),
    1.22                                       (@{cpat "?prec::nat"}, p),
    1.23 @@ -3663,9 +3663,9 @@
    1.24         else let
    1.25           val t = t
    1.26                |> HOLogic.mk_number @{typ nat}
    1.27 -              |> Thm.cterm_of (Proof_Context.theory_of ctxt)
    1.28 +              |> Proof_Context.cterm_of ctxt
    1.29           val s = vs |> map lookup_splitting |> hd
    1.30 -              |> Thm.cterm_of (Proof_Context.theory_of ctxt)
    1.31 +              |> Proof_Context.cterm_of ctxt
    1.32         in
    1.33           rtac (Thm.instantiate ([], [(@{cpat "?s::nat"}, s),
    1.34                                       (@{cpat "?t::nat"}, t),
     2.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Tue Mar 03 17:20:51 2015 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Tue Mar 03 19:08:04 2015 +0100
     2.3 @@ -1999,7 +1999,7 @@
     2.4    let 
     2.5      val vs = Term.add_frees t [];
     2.6      val t' = (term_of_fm vs o @{code linrqe} o fm_of_term vs) t;
     2.7 -  in (Thm.cterm_of (Proof_Context.theory_of ctxt) o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
     2.8 +  in (Proof_Context.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
     2.9  end;
    2.10  *}
    2.11  
     3.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Mar 03 17:20:51 2015 +0100
     3.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Mar 03 19:08:04 2015 +0100
     3.3 @@ -4155,7 +4155,7 @@
     3.4  in
     3.5  
     3.6    fn (ctxt, alternative, ty, ps, ct) =>
     3.7 -    cterm_of (Proof_Context.theory_of ctxt)
     3.8 +    Proof_Context.cterm_of ctxt
     3.9        (frpar_procedure alternative ty ps (term_of ct))
    3.10  
    3.11  end
     4.1 --- a/src/HOL/Decision_Procs/approximation.ML	Tue Mar 03 17:20:51 2015 +0100
     4.2 +++ b/src/HOL/Decision_Procs/approximation.ML	Tue Mar 03 19:08:04 2015 +0100
     4.3 @@ -92,7 +92,7 @@
     4.4    in t end
     4.5  
     4.6  fun apply_tactic ctxt term tactic =
     4.7 -  cterm_of (Proof_Context.theory_of ctxt) term
     4.8 +  Proof_Context.cterm_of ctxt term
     4.9    |> Goal.init
    4.10    |> SINGLE tactic
    4.11    |> the |> prems_of |> hd
    4.12 @@ -120,7 +120,7 @@
    4.13           |> foldr1 HOLogic.mk_conj))
    4.14  
    4.15  fun approx_arith prec ctxt t = realify t
    4.16 -     |> Thm.cterm_of (Proof_Context.theory_of ctxt)
    4.17 +     |> Proof_Context.cterm_of ctxt
    4.18       |> Reification.conv ctxt form_equations
    4.19       |> prop_of
    4.20       |> Logic.dest_equals |> snd
     5.1 --- a/src/HOL/Library/Old_SMT/old_smt_utils.ML	Tue Mar 03 17:20:51 2015 +0100
     5.2 +++ b/src/HOL/Library/Old_SMT/old_smt_utils.ML	Tue Mar 03 19:08:04 2015 +0100
     5.3 @@ -161,7 +161,7 @@
     5.4  
     5.5  (* certified terms *)
     5.6  
     5.7 -fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt)
     5.8 +fun certify ctxt = Proof_Context.cterm_of ctxt
     5.9  
    5.10  fun typ_of ct = #T (Thm.rep_cterm ct) 
    5.11  
     6.1 --- a/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Tue Mar 03 17:20:51 2015 +0100
     6.2 +++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Tue Mar 03 19:08:04 2015 +0100
     6.3 @@ -114,7 +114,7 @@
     6.4  val parse_id = Scan.one Symbol.is_letter ::: Scan.many Symbol.is_letdig >> implode
     6.5  
     6.6  fun parse_varpow ctxt = parse_id -- Scan.optional (str "^" |-- nat) 1 >>
     6.7 -  (fn (x, k) => (cterm_of (Proof_Context.theory_of ctxt) (Free (x, @{typ real})), k))
     6.8 +  (fn (x, k) => (Proof_Context.cterm_of ctxt (Free (x, @{typ real})), k))
     6.9  
    6.10  fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
    6.11    (fn xs => fold FuncUtil.Ctermfunc.update xs FuncUtil.Ctermfunc.empty)
     7.1 --- a/src/HOL/Library/simps_case_conv.ML	Tue Mar 03 17:20:51 2015 +0100
     7.2 +++ b/src/HOL/Library/simps_case_conv.ML	Tue Mar 03 19:08:04 2015 +0100
     7.3 @@ -97,7 +97,7 @@
     7.4    | import (thm :: thms) ctxt =
     7.5      let
     7.6        val fun_ct = strip_eq #> fst #> strip_comb #> fst #> Logic.mk_term
     7.7 -        #> Thm.cterm_of (Proof_Context.theory_of ctxt)
     7.8 +        #> Proof_Context.cterm_of ctxt
     7.9        val ct = fun_ct thm
    7.10        val cts = map fun_ct thms
    7.11        val pairs = map (fn s => (s,ct)) cts
     8.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Tue Mar 03 17:20:51 2015 +0100
     8.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Tue Mar 03 19:08:04 2015 +0100
     8.3 @@ -344,7 +344,7 @@
     8.4    fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
     8.5    fun mk_norm t = Thm.apply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
     8.6    fun mk_equals l r = Thm.apply (Thm.apply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
     8.7 -  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
     8.8 +  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
     8.9    val replace_conv = try_conv (rewrs_conv asl)
    8.10    val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv))
    8.11    val ges' =
     9.1 --- a/src/HOL/Nominal/nominal_induct.ML	Tue Mar 03 17:20:51 2015 +0100
     9.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Tue Mar 03 19:08:04 2015 +0100
     9.3 @@ -54,7 +54,7 @@
     9.4        end;
     9.5       val substs =
     9.6         map2 subst insts concls |> flat |> distinct (op =)
     9.7 -       |> map (apply2 (Thm.cterm_of (Proof_Context.theory_of ctxt)));
     9.8 +       |> map (apply2 (Proof_Context.cterm_of ctxt));
     9.9    in 
    9.10      (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) 
    9.11    end;
    10.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Tue Mar 03 17:20:51 2015 +0100
    10.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Tue Mar 03 19:08:04 2015 +0100
    10.3 @@ -281,7 +281,7 @@
    10.4      val qualify = Binding.qualify false
    10.5        (space_implode "_" (map (Long_Name.base_name o #1) defs));
    10.6      val names_atts' = map (apfst qualify) names_atts;
    10.7 -    val cert = cterm_of (Proof_Context.theory_of lthy');
    10.8 +    val cert = Proof_Context.cterm_of lthy';
    10.9  
   10.10      fun mk_idx eq =
   10.11        let
    11.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Mar 03 17:20:51 2015 +0100
    11.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Mar 03 19:08:04 2015 +0100
    11.3 @@ -1227,11 +1227,11 @@
    11.4                  val funTs = map (fn T => bdT --> T) ranTs;
    11.5                  val ran_bnfT = mk_bnf_T ranTs Calpha;
    11.6                  val (revTs, Ts) = `rev (bd_bnfT :: funTs);
    11.7 -                val cTs = map (SOME o certifyT lthy) [ran_bnfT, Library.foldr1 HOLogic.mk_prodT Ts];
    11.8 +                val cTs = map (SOME o Proof_Context.ctyp_of lthy) [ran_bnfT, Library.foldr1 HOLogic.mk_prodT Ts];
    11.9                  val tinst = fold (fn T => fn t => HOLogic.mk_split (Term.absdummy T t)) (tl revTs)
   11.10                    (Term.absdummy (hd revTs) (Term.list_comb (mk_bnf_map bdTs ranTs,
   11.11                      map Bound (live - 1 downto 0)) $ Bound live));
   11.12 -                val cts = [NONE, SOME (certify lthy tinst)];
   11.13 +                val cts = [NONE, SOME (Proof_Context.cterm_of lthy tinst)];
   11.14                in
   11.15                  Drule.instantiate' cTs cts @{thm surj_imp_ordLeq}
   11.16                end);
   11.17 @@ -1346,7 +1346,7 @@
   11.18          fun mk_rel_flip () =
   11.19            let
   11.20              val rel_conversep_thm = Lazy.force rel_conversep;
   11.21 -            val cts = map (SOME o certify lthy) Rs;
   11.22 +            val cts = map (SOME o Proof_Context.cterm_of lthy) Rs;
   11.23              val rel_conversep_thm' = cterm_instantiate_pos cts rel_conversep_thm;
   11.24            in
   11.25              unfold_thms lthy @{thms conversep_iff} (rel_conversep_thm' RS @{thm predicate2_eqD})
    12.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 03 17:20:51 2015 +0100
    12.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 03 19:08:04 2015 +0100
    12.3 @@ -476,7 +476,7 @@
    12.4    let
    12.5      val Rs = Term.add_vars (prop_of thm) [];
    12.6      val Rs' = rev (drop (length Rs - n) Rs);
    12.7 -    val cRs = map (fn f => (certify lthy (Var f), certify lthy (mk_flip f))) Rs';
    12.8 +    val cRs = map (fn f => (Proof_Context.cterm_of lthy (Var f), Proof_Context.cterm_of lthy (mk_flip f))) Rs';
    12.9    in
   12.10      Drule.cterm_instantiate cRs thm
   12.11    end;
   12.12 @@ -598,14 +598,14 @@
   12.13            Drule.dummy_thm
   12.14          else
   12.15            let val ctor' = mk_ctor Bs ctor in
   12.16 -            cterm_instantiate_pos [NONE, NONE, SOME (certify lthy ctor')] arg_cong
   12.17 +            cterm_instantiate_pos [NONE, NONE, SOME (Proof_Context.cterm_of lthy ctor')] arg_cong
   12.18            end;
   12.19  
   12.20        fun mk_cIn ctor k xs =
   12.21          let val absT = domain_type (fastype_of ctor) in
   12.22            mk_absumprod absT abs n k xs
   12.23            |> fp = Greatest_FP ? curry (op $) ctor
   12.24 -          |> certify lthy
   12.25 +          |> Proof_Context.cterm_of lthy
   12.26          end;
   12.27  
   12.28        val cxIns = map2 (mk_cIn ctor) ks xss;
   12.29 @@ -615,7 +615,7 @@
   12.30          fold_thms lthy [ctr_def']
   12.31            (unfold_thms lthy (o_apply :: pre_map_def ::
   12.32                 (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_map @ abs_inverses)
   12.33 -             (cterm_instantiate_pos (map (SOME o certify lthy) fs @ [SOME cxIn])
   12.34 +             (cterm_instantiate_pos (map (SOME o Proof_Context.cterm_of lthy) fs @ [SOME cxIn])
   12.35                  (if fp = Least_FP then fp_map_thm
   12.36                   else fp_map_thm RS ctor_cong RS (ctor_dtor RS sym RS trans))))
   12.37          |> singleton (Proof_Context.export names_lthy lthy);
   12.38 @@ -643,7 +643,7 @@
   12.39            (unfold_thms lthy (pre_rel_def :: abs_inverses @
   12.40                 (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @
   12.41                 @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]})
   12.42 -             (cterm_instantiate_pos (map (SOME o certify lthy) Rs @ [SOME cxIn, SOME cyIn])
   12.43 +             (cterm_instantiate_pos (map (SOME o Proof_Context.cterm_of lthy) Rs @ [SOME cxIn, SOME cyIn])
   12.44                  fp_rel_thm))
   12.45          |> postproc
   12.46          |> singleton (Proof_Context.export names_lthy lthy);
   12.47 @@ -734,7 +734,7 @@
   12.48                val goal = Logic.mk_implies (mk_Trueprop_mem (elem, set $ ta), thesis);
   12.49                val thm =
   12.50                  Goal.prove_sorry lthy [] (flat premss) goal (fn {context = ctxt, prems} =>
   12.51 -                  mk_set_cases_tac ctxt (certify ctxt ta) prems exhaust set_thms)
   12.52 +                  mk_set_cases_tac ctxt (Proof_Context.cterm_of ctxt ta) prems exhaust set_thms)
   12.53                  |> singleton (Proof_Context.export names_lthy lthy)
   12.54                  |> Thm.close_derivation
   12.55                  |> rotate_prems ~1;
   12.56 @@ -812,7 +812,7 @@
   12.57  
   12.58            fun prove goal =
   12.59              Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
   12.60 -              mk_rel_sel_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust (flat disc_thmss)
   12.61 +              mk_rel_sel_tac ctxt (Proof_Context.cterm_of ctxt ta) (Proof_Context.cterm_of ctxt tb) exhaust (flat disc_thmss)
   12.62                  (flat sel_thmss) rel_inject_thms distincts rel_distinct_thms live_nesting_rel_eqs)
   12.63              |> singleton (Proof_Context.export names_lthy lthy)
   12.64              |> Thm.close_derivation;
   12.65 @@ -846,7 +846,7 @@
   12.66            val goal = Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms, thesis);
   12.67            val thm =
   12.68              Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
   12.69 -              mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust injects
   12.70 +              mk_rel_cases_tac ctxt (Proof_Context.cterm_of ctxt ta) (Proof_Context.cterm_of ctxt tb) exhaust injects
   12.71                  rel_inject_thms distincts rel_distinct_thms live_nesting_rel_eqs)
   12.72              |> singleton (Proof_Context.export names_lthy lthy)
   12.73              |> Thm.close_derivation;
   12.74 @@ -920,7 +920,7 @@
   12.75            else
   12.76              Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
   12.77                (fn {context = ctxt, prems = _} =>
   12.78 -                 mk_map_disc_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss) map_thms)
   12.79 +                 mk_map_disc_iff_tac ctxt (Proof_Context.cterm_of ctxt ta) exhaust (flat disc_thmss) map_thms)
   12.80              |> Conjunction.elim_balanced (length goals)
   12.81              |> Proof_Context.export names_lthy lthy
   12.82              |> map Thm.close_derivation
   12.83 @@ -954,7 +954,7 @@
   12.84               else
   12.85                 Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
   12.86                   (fn {context = ctxt, prems = _} =>
   12.87 -                    mk_map_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss) map_thms
   12.88 +                    mk_map_sel_tac ctxt (Proof_Context.cterm_of ctxt ta) exhaust (flat disc_thmss) map_thms
   12.89                        (flat sel_thmss) live_nesting_map_id0s)
   12.90                 |> Conjunction.elim_balanced (length goals)
   12.91                 |> Proof_Context.export names_lthy lthy
   12.92 @@ -1013,7 +1013,7 @@
   12.93               else
   12.94                 Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
   12.95                   (fn {context = ctxt, prems = _} =>
   12.96 -                    mk_set_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
   12.97 +                    mk_set_sel_tac ctxt (Proof_Context.cterm_of ctxt ta) exhaust (flat disc_thmss)
   12.98                        (flat sel_thmss) set0_thms)
   12.99                 |> Conjunction.elim_balanced (length goals)
  12.100                 |> Proof_Context.export names_lthy lthy
  12.101 @@ -1302,7 +1302,7 @@
  12.102  
  12.103      val rel_induct0_thm =
  12.104        Goal.prove_sorry lthy [] prems goal (fn {context = ctxt, prems} =>
  12.105 -        mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (certify ctxt) IRs) exhausts ctor_defss
  12.106 +        mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (Proof_Context.cterm_of ctxt) IRs) exhausts ctor_defss
  12.107            ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs)
  12.108        |> singleton (Proof_Context.export names_lthy lthy)
  12.109        |> Thm.close_derivation;
  12.110 @@ -1560,7 +1560,7 @@
  12.111  
  12.112      val rel_coinduct0_thm =
  12.113        Goal.prove_sorry lthy [] prems goal (fn {context = ctxt, prems} =>
  12.114 -        mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (certify ctxt) IRs) prems
  12.115 +        mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (Proof_Context.cterm_of ctxt) IRs) prems
  12.116            (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars)
  12.117            (map (flat o #sel_thmss) ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects
  12.118            rel_pre_defs abs_inverses live_nesting_rel_eqs)
  12.119 @@ -1644,7 +1644,7 @@
  12.120          val thm =
  12.121            Goal.prove_sorry lthy [] prems (HOLogic.mk_Trueprop concl)
  12.122              (fn {context = ctxt, prems} =>
  12.123 -               mk_set_induct0_tac ctxt (map (certify ctxt'') Ps) prems dtor_set_inducts exhausts
  12.124 +               mk_set_induct0_tac ctxt (map (Proof_Context.cterm_of ctxt'') Ps) prems dtor_set_inducts exhausts
  12.125                   set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses)
  12.126            |> singleton (Proof_Context.export ctxt'' ctxt)
  12.127            |> Thm.close_derivation;
  12.128 @@ -1819,7 +1819,7 @@
  12.129  
  12.130          val goalss = @{map 6} (map2 oooo mk_goal) cs cpss gcorecs ns kss discss;
  12.131  
  12.132 -        fun mk_case_split' cp = Drule.instantiate' [] [SOME (certify lthy cp)] @{thm case_split};
  12.133 +        fun mk_case_split' cp = Drule.instantiate' [] [SOME (Proof_Context.cterm_of lthy cp)] @{thm case_split};
  12.134  
  12.135          val case_splitss' = map (map mk_case_split') cpss;
  12.136  
  12.137 @@ -1845,8 +1845,8 @@
  12.138        let
  12.139          val (domT, ranT) = dest_funT (fastype_of sel);
  12.140          val arg_cong' =
  12.141 -          Drule.instantiate' (map (SOME o certifyT lthy) [domT, ranT])
  12.142 -            [NONE, NONE, SOME (certify lthy sel)] arg_cong
  12.143 +          Drule.instantiate' (map (SOME o Proof_Context.ctyp_of lthy) [domT, ranT])
  12.144 +            [NONE, NONE, SOME (Proof_Context.cterm_of lthy sel)] arg_cong
  12.145            |> Thm.varifyT_global;
  12.146          val sel_thm' = sel_thm RSN (2, trans);
  12.147        in
  12.148 @@ -2141,8 +2141,8 @@
  12.149                          (mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w)));
  12.150                    in
  12.151                      Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
  12.152 -                      mk_ctor_iff_dtor_tac ctxt (map (SOME o certifyT lthy) [ctr_absT, fpT])
  12.153 -                        (certify lthy ctor) (certify lthy dtor) ctor_dtor dtor_ctor)
  12.154 +                      mk_ctor_iff_dtor_tac ctxt (map (SOME o Proof_Context.ctyp_of lthy) [ctr_absT, fpT])
  12.155 +                        (Proof_Context.cterm_of lthy ctor) (Proof_Context.cterm_of lthy dtor) ctor_dtor dtor_ctor)
  12.156                      |> Morphism.thm phi
  12.157                      |> Thm.close_derivation
  12.158                    end;
  12.159 @@ -2233,7 +2233,7 @@
  12.160        let val (Rs, Ss, goals, names_lthy) = mk_co_rec_transfer_goals lthy recs in
  12.161          Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
  12.162            (fn {context = ctxt, prems = _} =>
  12.163 -             mk_rec_transfer_tac ctxt nn ns (map (certify ctxt) Ss) (map (certify ctxt) Rs) xsssss
  12.164 +             mk_rec_transfer_tac ctxt nn ns (map (Proof_Context.cterm_of ctxt) Ss) (map (Proof_Context.cterm_of ctxt) Rs) xsssss
  12.165                 rec_defs xtor_co_rec_transfers pre_rel_defs live_nesting_rel_eqs)
  12.166          |> Conjunction.elim_balanced nn
  12.167          |> Proof_Context.export names_lthy lthy
  12.168 @@ -2385,7 +2385,7 @@
  12.169        in
  12.170          Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
  12.171            (fn {context = ctxt, prems = _} =>
  12.172 -             mk_corec_transfer_tac ctxt (map (certify ctxt) Ss) (map (certify ctxt) Rs)
  12.173 +             mk_corec_transfer_tac ctxt (map (Proof_Context.cterm_of ctxt) Ss) (map (Proof_Context.cterm_of ctxt) Rs)
  12.174                 type_definitions corec_defs xtor_co_rec_transfers pre_rel_defs
  12.175                 live_nesting_rel_eqs (flat pgss) pss qssss gssss)
  12.176          |> Conjunction.elim_balanced (length goals)
    13.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Mar 03 17:20:51 2015 +0100
    13.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Mar 03 19:08:04 2015 +0100
    13.3 @@ -97,7 +97,7 @@
    13.4      val fs = Term.add_vars (prop_of thm) []
    13.5        |> filter (fn (_, Type (@{type_name fun}, [_, T'])) => T' <> HOLogic.boolT | _ => false);
    13.6      fun mk_cfp (f as (_, T)) =
    13.7 -      (certify ctxt (Var f), certify ctxt (mk_proj T (num_binder_types T) k));
    13.8 +      (Proof_Context.cterm_of ctxt (Var f), Proof_Context.cterm_of ctxt (mk_proj T (num_binder_types T) k));
    13.9      val cfps = map mk_cfp fs;
   13.10    in
   13.11      Drule.cterm_instantiate cfps thm
    14.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Mar 03 17:20:51 2015 +0100
    14.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Mar 03 19:08:04 2015 +0100
    14.3 @@ -191,7 +191,7 @@
    14.4            case_fp fp (snd o Term.dest_comb) (snd o Term.dest_comb o fst o Term.dest_comb);
    14.5          val raw_phis = map (extract o HOLogic.dest_Trueprop o Thm.concl_of) rel_xtor_co_inducts;
    14.6          val thetas = AList.group (op =)
    14.7 -          (mutual_cliques ~~ map (apply2 (certify lthy)) (raw_phis ~~ pre_phis));
    14.8 +          (mutual_cliques ~~ map (apply2 (Proof_Context.cterm_of lthy)) (raw_phis ~~ pre_phis));
    14.9        in
   14.10          map2 (Drule.cterm_instantiate o the o AList.lookup (op =) thetas)
   14.11          mutual_cliques rel_xtor_co_inducts
   14.12 @@ -214,7 +214,7 @@
   14.13              fun mk_Grp_id P =
   14.14                let val T = domain_type (fastype_of P);
   14.15                in mk_Grp (HOLogic.Collect_const T $ P) (HOLogic.id_const T) end;
   14.16 -            val cts = map (SOME o certify lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps);
   14.17 +            val cts = map (SOME o Proof_Context.cterm_of lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps);
   14.18              fun mk_fp_type_copy_thms thm = map (curry op RS thm)
   14.19                @{thms type_copy_Abs_o_Rep type_copy_vimage2p_Grp_Rep};
   14.20              fun mk_type_copy_thms thm = map (curry op RS thm)
   14.21 @@ -235,7 +235,7 @@
   14.22            end
   14.23        | Greatest_FP =>
   14.24            let
   14.25 -            val cts = NONE :: map (SOME o certify lthy) (map HOLogic.eq_const As);
   14.26 +            val cts = NONE :: map (SOME o Proof_Context.cterm_of lthy) (map HOLogic.eq_const As);
   14.27            in
   14.28              cterm_instantiate_pos cts xtor_rel_co_induct
   14.29              |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @
    15.1 --- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Tue Mar 03 17:20:51 2015 +0100
    15.2 +++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Tue Mar 03 19:08:04 2015 +0100
    15.3 @@ -44,7 +44,7 @@
    15.4          val else_branch = Var (("e", j), T);
    15.5          val lam = Term.lambda cond (mk_If cond then_branch else_branch);
    15.6        in
    15.7 -        cterm_instantiate_pos [SOME (certify ctxt lam)] thm
    15.8 +        cterm_instantiate_pos [SOME (Proof_Context.cterm_of ctxt lam)] thm
    15.9        end;
   15.10  
   15.11      val transfer_rules =
    16.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Mar 03 17:20:51 2015 +0100
    16.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Mar 03 19:08:04 2015 +0100
    16.3 @@ -578,7 +578,7 @@
    16.4      val n = Thm.nprems_of coind;
    16.5      val m = Thm.nprems_of (hd rel_monos) - n;
    16.6      fun mk_inst phi = (phi, mk_union (phi, HOLogic.eq_const (fst (dest_pred2T (fastype_of phi)))))
    16.7 -      |> apply2 (certify ctxt);
    16.8 +      |> apply2 (Proof_Context.cterm_of ctxt);
    16.9      val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map (mk_inst o Var);
   16.10      fun mk_unfold rel_eq rel_mono =
   16.11        let
    17.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Mar 03 17:20:51 2015 +0100
    17.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Mar 03 19:08:04 2015 +0100
    17.3 @@ -1080,7 +1080,7 @@
    17.4          val goal = list_all_free (kl :: zs)
    17.5            (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
    17.6  
    17.7 -        val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
    17.8 +        val cts = map (SOME o Proof_Context.cterm_of lthy) [Term.absfree nat' goal, nat];
    17.9  
   17.10          val length_Lev =
   17.11            Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
   17.12 @@ -1115,8 +1115,8 @@
   17.13              Library.foldr1 HOLogic.mk_conj
   17.14                (map2 (mk_conjunct i z) ks zs_copy)) ks zs));
   17.15  
   17.16 -        val cTs = [SOME (certifyT lthy sum_sbdT)];
   17.17 -        val cts = map (SOME o certify lthy) [Term.absfree kl' goal, kl];
   17.18 +        val cTs = [SOME (Proof_Context.ctyp_of lthy sum_sbdT)];
   17.19 +        val cts = map (SOME o Proof_Context.cterm_of lthy) [Term.absfree kl' goal, kl];
   17.20  
   17.21          val rv_last =
   17.22            Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
   17.23 @@ -1153,7 +1153,7 @@
   17.24          val goal = list_all_free (kl :: zs @ zs_copy @ zs_copy2)
   17.25            (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
   17.26  
   17.27 -        val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
   17.28 +        val cts = map (SOME o Proof_Context.cterm_of lthy) [Term.absfree nat' goal, nat];
   17.29  
   17.30          val set_Lev =
   17.31            Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
   17.32 @@ -1192,7 +1192,7 @@
   17.33          val goal = list_all_free (kl :: k :: zs @ zs_copy)
   17.34            (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
   17.35  
   17.36 -        val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
   17.37 +        val cts = map (SOME o Proof_Context.cterm_of lthy) [Term.absfree nat' goal, nat];
   17.38  
   17.39          val set_image_Lev =
   17.40            Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
   17.41 @@ -1867,7 +1867,7 @@
   17.42                    Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls
   17.43  
   17.44                  val ctss =
   17.45 -                  map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls;
   17.46 +                  map (fn phi => map (SOME o Proof_Context.cterm_of lthy) [Term.absfree nat' phi, nat]) concls;
   17.47                in
   17.48                  @{map 4} (fn goal => fn cts => fn col_0s => fn col_Sucs =>
   17.49                    Goal.prove_sorry lthy [] [] goal
   17.50 @@ -1952,10 +1952,10 @@
   17.51                maps (map (fn thm => thm RS @{thm subset_Collect_iff})) dtor_Jset_incl_thmss @
   17.52                  @{thms subset_Collect_iff[OF subset_refl]};
   17.53  
   17.54 -            val cTs = map (SOME o certifyT lthy) params';
   17.55 +            val cTs = map (SOME o Proof_Context.ctyp_of lthy) params';
   17.56              fun mk_induct_tinst phis jsets y y' =
   17.57                @{map 4} (fn phi => fn jset => fn Jz => fn Jz' =>
   17.58 -                SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y',
   17.59 +                SOME (Proof_Context.cterm_of lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y',
   17.60                    HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz))))))
   17.61                phis jsets Jzs Jzs';
   17.62            in
   17.63 @@ -2024,7 +2024,7 @@
   17.64              val goals = @{map 3} mk_goal fs colss colss';
   17.65  
   17.66              val ctss =
   17.67 -              map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals;
   17.68 +              map (fn phi => map (SOME o Proof_Context.cterm_of lthy) [Term.absfree nat' phi, nat]) goals;
   17.69  
   17.70              val thms =
   17.71                @{map 4} (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
   17.72 @@ -2047,7 +2047,7 @@
   17.73  
   17.74              val goals = map (mk_goal Jbds) colss;
   17.75  
   17.76 -            val ctss = map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat])
   17.77 +            val ctss = map (fn phi => map (SOME o Proof_Context.cterm_of lthy) [Term.absfree nat' phi, nat])
   17.78                (map (mk_goal (replicate n sbd)) colss);
   17.79  
   17.80              val thms =
   17.81 @@ -2064,7 +2064,7 @@
   17.82  
   17.83          val map_cong0_thms =
   17.84            let
   17.85 -            val cTs = map (SOME o certifyT lthy o
   17.86 +            val cTs = map (SOME o Proof_Context.ctyp_of lthy o
   17.87                Term.typ_subst_atomic (passiveAs ~~ passiveBs) o TFree) coinduct_params;
   17.88  
   17.89              fun mk_prem z set f g y y' =
   17.90 @@ -2086,7 +2086,7 @@
   17.91                HOLogic.mk_exists (x, T, mk_coind_body sets z' z fmap gmap y y_copy)
   17.92                |> Term.absfree y'_copy
   17.93                |> Term.absfree y'
   17.94 -              |> certify lthy;
   17.95 +              |> Proof_Context.cterm_of lthy;
   17.96  
   17.97              val cphis = @{map 9} mk_cphi
   17.98                Jsetss_by_bnf Jzs' Jzs fs_Jmaps fs_copy_Jmaps Jys' Jys Jys'_copy Jys_copy;
   17.99 @@ -2189,9 +2189,9 @@
  17.100                activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds;
  17.101            fun mk_cts zs z's phis =
  17.102              @{map 3} (fn z => fn z' => fn phi =>
  17.103 -              SOME (certify lthy (fold_rev (Term.absfree o Term.dest_Free) [z', z] phi)))
  17.104 +              SOME (Proof_Context.cterm_of lthy (fold_rev (Term.absfree o Term.dest_Free) [z', z] phi)))
  17.105              zs z's phis @
  17.106 -            map (SOME o certify lthy) (splice z's zs);
  17.107 +            map (SOME o Proof_Context.cterm_of lthy) (splice z's zs);
  17.108            val cts1 = mk_cts Jzs Jzs_copy coind1_phis;
  17.109            val cts2 = mk_cts Jz's Jz's_copy coind2_phis;
  17.110  
  17.111 @@ -2228,9 +2228,9 @@
  17.112              Jphis abs fstABs sndABs;
  17.113            val ctss = map2 (fn ab' => fn phis =>
  17.114                map2 (fn z' => fn phi =>
  17.115 -                SOME (certify lthy (Term.absfree ab' (Term.absfree z' phi))))
  17.116 +                SOME (Proof_Context.cterm_of lthy (Term.absfree ab' (Term.absfree z' phi))))
  17.117                zip_zs' phis @
  17.118 -              map (SOME o certify lthy) zip_zs)
  17.119 +              map (SOME o Proof_Context.cterm_of lthy) zip_zs)
  17.120              abs' helper_ind_phiss;
  17.121            fun mk_helper_ind_concl ab' z ind_phi set =
  17.122              mk_Ball (set $ z) (Term.absfree ab' ind_phi);
    18.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Tue Mar 03 17:20:51 2015 +0100
    18.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Tue Mar 03 19:08:04 2015 +0100
    18.3 @@ -43,7 +43,7 @@
    18.4      val fs = Term.add_vars (prop_of thm) [] |> filter (can dest_funT o snd);
    18.5      fun find s = find_index (curry (op =) s) frees;
    18.6      fun mk_cfp (f as ((s, _), T)) =
    18.7 -      (certify ctxt (Var f), certify ctxt (mk_proj T num_frees (find s)));
    18.8 +      (Proof_Context.cterm_of ctxt (Var f), Proof_Context.cterm_of ctxt (mk_proj T num_frees (find s)));
    18.9      val cfps = map mk_cfp fs;
   18.10    in
   18.11      Drule.cterm_instantiate cfps thm
   18.12 @@ -154,7 +154,7 @@
   18.13      let
   18.14        val s = Name.uu;
   18.15        val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
   18.16 -      val split' = Drule.instantiate' [] [SOME (certify ctxt eq)] split;
   18.17 +      val split' = Drule.instantiate' [] [SOME (Proof_Context.cterm_of ctxt eq)] split;
   18.18      in
   18.19        Thm.generalize ([], [s]) (Thm.maxidx_of split' + 1) split'
   18.20      end
    19.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Mar 03 17:20:51 2015 +0100
    19.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Mar 03 19:08:04 2015 +0100
    19.3 @@ -607,8 +607,8 @@
    19.4  
    19.5          fun mk_card_conjunct min_alg = mk_ordLeq (mk_card_of min_alg) Asuc_bd;
    19.6          val card_conjunction = Library.foldr1 HOLogic.mk_conj (map mk_card_conjunct min_algss);
    19.7 -        val card_cT = certifyT lthy suc_bdT;
    19.8 -        val card_ct = certify lthy (Term.absfree idx' card_conjunction);
    19.9 +        val card_cT = Proof_Context.ctyp_of lthy suc_bdT;
   19.10 +        val card_ct = Proof_Context.cterm_of lthy (Term.absfree idx' card_conjunction);
   19.11  
   19.12          val card_of =
   19.13            Goal.prove_sorry lthy [] []
   19.14 @@ -622,8 +622,8 @@
   19.15  
   19.16          val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
   19.17          val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_leq min_algss Bs);
   19.18 -        val least_cT = certifyT lthy suc_bdT;
   19.19 -        val least_ct = certify lthy (Term.absfree idx' least_conjunction);
   19.20 +        val least_cT = Proof_Context.ctyp_of lthy suc_bdT;
   19.21 +        val least_ct = Proof_Context.cterm_of lthy (Term.absfree idx' least_conjunction);
   19.22  
   19.23          val least =
   19.24            (Goal.prove_sorry lthy [] []
   19.25 @@ -779,7 +779,7 @@
   19.26  
   19.27      val car_inits = map (mk_min_alg str_inits) ks;
   19.28  
   19.29 -    val alg_init_thm = cterm_instantiate_pos (map (SOME o certify lthy) str_inits) alg_min_alg_thm;
   19.30 +    val alg_init_thm = cterm_instantiate_pos (map (SOME o Proof_Context.cterm_of lthy) str_inits) alg_min_alg_thm;
   19.31  
   19.32      val alg_select_thm = Goal.prove_sorry lthy [] []
   19.33        (HOLogic.mk_Trueprop (mk_Ball II
   19.34 @@ -812,7 +812,7 @@
   19.35          fun mk_fun_eq f g x = HOLogic.mk_eq (f $ x, g $ x);
   19.36          val unique = HOLogic.mk_Trueprop
   19.37            (Library.foldr1 HOLogic.mk_conj (@{map 3} mk_fun_eq init_fs init_fs_copy init_xs));
   19.38 -        val cts = map (certify lthy) ss;
   19.39 +        val cts = map (Proof_Context.cterm_of lthy) ss;
   19.40          val unique_mor =
   19.41            Goal.prove_sorry lthy [] [] (Logic.list_implies (prems @ mor_prems, unique))
   19.42              (K (mk_init_unique_mor_tac cts m alg_def alg_init_thm least_min_alg_thms
   19.43 @@ -946,7 +946,7 @@
   19.44            |> Thm.close_derivation;
   19.45  
   19.46          fun mk_ct initFT str abs = Term.absdummy initFT (abs $ (str $ Bound 0))
   19.47 -        val cts = @{map 3} (certify lthy ooo mk_ct) init_FTs str_inits Abs_Ts;
   19.48 +        val cts = @{map 3} (Proof_Context.cterm_of lthy ooo mk_ct) init_FTs str_inits Abs_Ts;
   19.49  
   19.50          val mor_Abs =
   19.51            Goal.prove_sorry lthy [] []
   19.52 @@ -1020,8 +1020,8 @@
   19.53      val mor_fold_thm =
   19.54        let
   19.55          val mor_cong = mor_cong_thm OF (map (mk_nth_conv n) ks);
   19.56 -        val cT = certifyT lthy foldT;
   19.57 -        val ct = certify lthy fold_fun
   19.58 +        val cT = Proof_Context.ctyp_of lthy foldT;
   19.59 +        val ct = Proof_Context.cterm_of lthy fold_fun
   19.60        in
   19.61          Goal.prove_sorry lthy [] []
   19.62            (HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_fold Ts ss) ks)))
   19.63 @@ -1244,7 +1244,7 @@
   19.64          rev (Term.add_tfrees goal []))
   19.65        end;
   19.66  
   19.67 -    val cTs = map (SOME o certifyT lthy o TFree) induct_params;
   19.68 +    val cTs = map (SOME o Proof_Context.ctyp_of lthy o TFree) induct_params;
   19.69  
   19.70      val weak_ctor_induct_thms =
   19.71        let fun insts i = (replicate (i - 1) TrueI) @ (asm_rl :: replicate (n - i) TrueI);
   19.72 @@ -1276,7 +1276,7 @@
   19.73            (@{map 3} mk_concl phi2s Izs1 Izs2));
   19.74          fun mk_t phi (z1, z1') (z2, z2') =
   19.75            Term.absfree z1' (HOLogic.mk_all (fst z2', snd z2', phi $ z1 $ z2));
   19.76 -        val cts = @{map 3} (SOME o certify lthy ooo mk_t) phi2s (Izs1 ~~ Izs1') (Izs2 ~~ Izs2');
   19.77 +        val cts = @{map 3} (SOME o Proof_Context.cterm_of lthy ooo mk_t) phi2s (Izs1 ~~ Izs1') (Izs2 ~~ Izs2');
   19.78          val goal = Logic.list_implies (prems, concl);
   19.79        in
   19.80          (Goal.prove_sorry lthy [] [] goal
   19.81 @@ -1552,7 +1552,7 @@
   19.82  
   19.83          val timer = time (timer "set functions for the new datatypes");
   19.84  
   19.85 -        val cxs = map (SOME o certify lthy) Izs;
   19.86 +        val cxs = map (SOME o Proof_Context.cterm_of lthy) Izs;
   19.87          val Isetss_by_range' =
   19.88            map (map (Term.subst_atomic_types (passiveAs ~~ passiveBs))) Isetss_by_range;
   19.89  
   19.90 @@ -1561,10 +1561,10 @@
   19.91              fun mk_set_map0 f map z set set' =
   19.92                HOLogic.mk_eq (mk_image f $ (set $ z), set' $ (map $ z));
   19.93  
   19.94 -            fun mk_cphi f map z set set' = certify lthy
   19.95 +            fun mk_cphi f map z set set' = Proof_Context.cterm_of lthy
   19.96                (Term.absfree (dest_Free z) (mk_set_map0 f map z set set'));
   19.97  
   19.98 -            val csetss = map (map (certify lthy)) Isetss_by_range';
   19.99 +            val csetss = map (map (Proof_Context.cterm_of lthy)) Isetss_by_range';
  19.100  
  19.101              val cphiss = @{map 3} (fn f => fn sets => fn sets' =>
  19.102                (@{map 4} (mk_cphi f) fs_Imaps Izs sets sets')) fs Isetss_by_range Isetss_by_range';
  19.103 @@ -1594,7 +1594,7 @@
  19.104            let
  19.105              fun mk_set_bd z bd set = mk_ordLeq (mk_card_of (set $ z)) bd;
  19.106  
  19.107 -            fun mk_cphi z set = certify lthy (Term.absfree (dest_Free z) (mk_set_bd z sbd0 set));
  19.108 +            fun mk_cphi z set = Proof_Context.cterm_of lthy (Term.absfree (dest_Free z) (mk_set_bd z sbd0 set));
  19.109  
  19.110              val cphiss = map (map2 mk_cphi Izs) Isetss_by_range;
  19.111  
  19.112 @@ -1630,7 +1630,7 @@
  19.113                  HOLogic.mk_eq (fmap $ z, gmap $ z));
  19.114  
  19.115              fun mk_cphi sets z fmap gmap =
  19.116 -              certify lthy (Term.absfree (dest_Free z) (mk_map_cong0 sets z fmap gmap));
  19.117 +              Proof_Context.cterm_of lthy (Term.absfree (dest_Free z) (mk_map_cong0 sets z fmap gmap));
  19.118  
  19.119              val cphis = @{map 4} mk_cphi Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps;
  19.120  
  19.121 @@ -1691,9 +1691,9 @@
  19.122                  Irelpsi12 $ Iz1 $ Iz2);
  19.123              val goals = @{map 5} mk_le_Irel_OO Irelpsi1s Irelpsi2s Irelpsi12s Izs1 Izs2;
  19.124  
  19.125 -            val cTs = map (SOME o certifyT lthy o TFree) induct2_params;
  19.126 -            val cxs = map (SOME o certify lthy) (splice Izs1 Izs2);
  19.127 -            fun mk_cphi z1 z2 goal = SOME (certify lthy (Term.absfree z1 (Term.absfree z2 goal)));
  19.128 +            val cTs = map (SOME o Proof_Context.ctyp_of lthy o TFree) induct2_params;
  19.129 +            val cxs = map (SOME o Proof_Context.cterm_of lthy) (splice Izs1 Izs2);
  19.130 +            fun mk_cphi z1 z2 goal = SOME (Proof_Context.cterm_of lthy (Term.absfree z1 (Term.absfree z2 goal)));
  19.131              val cphis = @{map 3} mk_cphi Izs1' Izs2' goals;
  19.132              val induct = Drule.instantiate' cTs (cphis @ cxs) ctor_induct2_thm;
  19.133  
    20.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Mar 03 17:20:51 2015 +0100
    20.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Mar 03 19:08:04 2015 +0100
    20.3 @@ -273,7 +273,7 @@
    20.4                HOLogic.mk_Trueprop (BNF_LFP_Util.mk_not_eq (list_comb (size, xs)) HOLogic.zero);
    20.5              val thm =
    20.6                Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
    20.7 -                mk_size_neq ctxt (map (certify lthy2) xs)
    20.8 +                mk_size_neq ctxt (map (Proof_Context.cterm_of lthy2) xs)
    20.9                  (#exhaust (#ctr_sugar (#fp_ctr_sugar fp_sugar))) size_thms)
   20.10                |> single
   20.11                |> Proof_Context.export names_lthy2 lthy2
    21.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Mar 03 17:20:51 2015 +0100
    21.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Mar 03 19:08:04 2015 +0100
    21.3 @@ -679,10 +679,10 @@
    21.4        let
    21.5          val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat;
    21.6  
    21.7 -        val rho_As = map (apply2 (certifyT lthy)) (map Logic.varifyT_global As ~~ As);
    21.8 +        val rho_As = map (apply2 (Proof_Context.ctyp_of lthy)) (map Logic.varifyT_global As ~~ As);
    21.9  
   21.10          fun inst_thm t thm =
   21.11 -          Drule.instantiate' [] [SOME (certify lthy t)]
   21.12 +          Drule.instantiate' [] [SOME (Proof_Context.cterm_of lthy t)]
   21.13              (Thm.instantiate (rho_As, []) (Drule.zero_var_indexes thm));
   21.14  
   21.15          val uexhaust_thm = inst_thm u exhaust_thm;
   21.16 @@ -997,7 +997,7 @@
   21.17                      mk_Trueprop_eq (udisc, list_comb (casexBool, mk_case_args n) $ u)) udiscs;
   21.18                  in
   21.19                    Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
   21.20 -                    (fn {context = ctxt, ...} => mk_disc_eq_case_tac ctxt (certify ctxt u)
   21.21 +                    (fn {context = ctxt, ...} => mk_disc_eq_case_tac ctxt (Proof_Context.cterm_of ctxt u)
   21.22                         exhaust_thm (flat nontriv_disc_thmss) distinct_thms case_thms)
   21.23                    |> Conjunction.elim_balanced (length goals)
   21.24                    |> Proof_Context.export names_lthy lthy
   21.25 @@ -1020,7 +1020,7 @@
   21.26              val goal = mk_Trueprop_eq (h $ ufcase, list_comb (casexC, args) $ u);
   21.27            in
   21.28              Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   21.29 -              mk_case_distrib_tac ctxt (certify ctxt u) exhaust_thm case_thms)
   21.30 +              mk_case_distrib_tac ctxt (Proof_Context.cterm_of ctxt u) exhaust_thm case_thms)
   21.31              |> singleton (Proof_Context.export names_lthy lthy)
   21.32              |> Thm.close_derivation
   21.33            end;
    22.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Tue Mar 03 17:20:51 2015 +0100
    22.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Tue Mar 03 19:08:04 2015 +0100
    22.3 @@ -62,9 +62,6 @@
    22.4    val cterm_instantiate_pos: cterm option list -> thm -> thm
    22.5    val unfold_thms: Proof.context -> thm list -> thm -> thm
    22.6  
    22.7 -  val certifyT: Proof.context -> typ -> ctyp
    22.8 -  val certify: Proof.context -> term -> cterm
    22.9 -
   22.10    val name_noted_thms: string -> string -> (string * thm list) list -> (string * thm list) list
   22.11    val substitute_noted_thm: (string * thm list) list -> morphism
   22.12  
   22.13 @@ -226,10 +223,6 @@
   22.14  
   22.15  fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
   22.16  
   22.17 -(*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
   22.18 -val certifyT = Thm.ctyp_of o Proof_Context.theory_of;
   22.19 -val certify = Thm.cterm_of o Proof_Context.theory_of;
   22.20 -
   22.21  fun name_noted_thms _ _ [] = []
   22.22    | name_noted_thms qualifier base ((local_name, thms) :: noted) =
   22.23      if Long_Name.base_name local_name = base then
    23.1 --- a/src/HOL/Tools/Function/function_context_tree.ML	Tue Mar 03 17:20:51 2015 +0100
    23.2 +++ b/src/HOL/Tools/Function/function_context_tree.ML	Tue Mar 03 19:08:04 2015 +0100
    23.3 @@ -149,7 +149,7 @@
    23.4              val (r, dep, branches) = find_cong_rule ctxt fvar h congs_deps t
    23.5              fun subtree (ctxt', fixes, assumes, st) =
    23.6                ((fixes,
    23.7 -                map (Thm.assume o cterm_of (Proof_Context.theory_of ctxt)) assumes),
    23.8 +                map (Thm.assume o Proof_Context.cterm_of ctxt) assumes),
    23.9                 mk_tree' ctxt' st)
   23.10            in
   23.11              Cong (r, dep, map subtree branches)
    24.1 --- a/src/HOL/Tools/Function/function_core.ML	Tue Mar 03 17:20:51 2015 +0100
    24.2 +++ b/src/HOL/Tools/Function/function_core.ML	Tue Mar 03 19:08:04 2015 +0100
    24.3 @@ -183,7 +183,7 @@
    24.4      val Globals {h, ...} = globals
    24.5  
    24.6      val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
    24.7 -    val cert = Thm.cterm_of (Proof_Context.theory_of ctxt)
    24.8 +    val cert = Proof_Context.cterm_of ctxt
    24.9  
   24.10      (* Instantiate the GIntro thm with "f" and import into the clause context. *)
   24.11      val lGI = GIntro_thm
   24.12 @@ -453,7 +453,7 @@
   24.13            [] (* no special monos *)
   24.14        ||> Local_Theory.restore_naming lthy
   24.15  
   24.16 -    val cert = cterm_of (Proof_Context.theory_of lthy)
   24.17 +    val cert = Proof_Context.cterm_of lthy
   24.18      fun requantify orig_intro thm =
   24.19        let
   24.20          val (qs, t) = dest_all_all orig_intro
   24.21 @@ -871,7 +871,7 @@
   24.22      val newthy = Proof_Context.theory_of lthy
   24.23      val clauses = map (transfer_clause_ctx newthy) clauses
   24.24  
   24.25 -    val cert = cterm_of (Proof_Context.theory_of lthy)
   24.26 +    val cert = Proof_Context.cterm_of lthy
   24.27  
   24.28      val xclauses = PROFILE "xclauses"
   24.29        (@{map 7} (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
    25.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Tue Mar 03 17:20:51 2015 +0100
    25.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Tue Mar 03 19:08:04 2015 +0100
    25.3 @@ -354,7 +354,7 @@
    25.4      val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt'
    25.5      val R = Free (Rn, mk_relT ST)
    25.6      val x = Free (xn, ST)
    25.7 -    val cert = cterm_of (Proof_Context.theory_of ctxt)
    25.8 +    val cert = Proof_Context.cterm_of ctxt
    25.9  
   25.10      val ineqss = mk_ineqs R scheme |> map (map (apply2 (Thm.assume o cert)))
   25.11      val complete =
    26.1 --- a/src/HOL/Tools/Function/measure_functions.ML	Tue Mar 03 17:20:51 2015 +0100
    26.2 +++ b/src/HOL/Tools/Function/measure_functions.ML	Tue Mar 03 19:08:04 2015 +0100
    26.3 @@ -20,7 +20,7 @@
    26.4  fun find_measures ctxt T =
    26.5    DEPTH_SOLVE (resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems measure_function})) 1)
    26.6      (HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT)))
    26.7 -     |> cterm_of (Proof_Context.theory_of ctxt) |> Goal.init)
    26.8 +     |> Proof_Context.cterm_of ctxt |> Goal.init)
    26.9    |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
   26.10    |> Seq.list_of
   26.11  
    27.1 --- a/src/HOL/Tools/Function/mutual.ML	Tue Mar 03 17:20:51 2015 +0100
    27.2 +++ b/src/HOL/Tools/Function/mutual.ML	Tue Mar 03 19:08:04 2015 +0100
    27.3 @@ -209,7 +209,7 @@
    27.4  
    27.5  fun mutual_induct_rules ctxt induct all_f_defs (Mutual {n, ST, parts, ...}) =
    27.6    let
    27.7 -    val cert = cterm_of (Proof_Context.theory_of ctxt)
    27.8 +    val cert = Proof_Context.cterm_of ctxt
    27.9      val newPs =
   27.10        map2 (fn Pname => fn MutualPart {cargTs, ...} =>
   27.11            Free (Pname, cargTs ---> HOLogic.boolT))
   27.12 @@ -259,7 +259,7 @@
   27.13      val argsT = fastype_of (HOLogic.mk_tuple arg_vars)
   27.14      val (args, name_ctxt) = mk_var "x" argsT name_ctxt
   27.15      
   27.16 -    val cert = cterm_of (Proof_Context.theory_of ctxt)
   27.17 +    val cert = Proof_Context.cterm_of ctxt
   27.18      val P = mk_var "P" @{typ "bool"} name_ctxt |> fst |> cert
   27.19      val sumtree_inj = Sum_Tree.mk_inj ST n i args
   27.20  
    28.1 --- a/src/HOL/Tools/Function/partial_function.ML	Tue Mar 03 17:20:51 2015 +0100
    28.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Tue Mar 03 19:08:04 2015 +0100
    28.3 @@ -168,7 +168,7 @@
    28.4    curry induction predicate *)
    28.5  fun specialize_fixp_induct ctxt args fT fT_uc F curry uncurry mono_thm f_def rule =
    28.6    let
    28.7 -    val cert = Thm.cterm_of (Proof_Context.theory_of ctxt)
    28.8 +    val cert = Proof_Context.cterm_of ctxt
    28.9      val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
   28.10      val P_inst = Abs ("f", fT_uc, Free (P, fT --> HOLogic.boolT) $ (curry $ Bound 0))
   28.11    in 
   28.12 @@ -187,7 +187,7 @@
   28.13  
   28.14  fun mk_curried_induct args ctxt inst_rule =
   28.15    let
   28.16 -    val cert = Thm.cterm_of (Proof_Context.theory_of ctxt)
   28.17 +    val cert = Proof_Context.cterm_of ctxt
   28.18      val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
   28.19  
   28.20      val split_paired_all_conv =
   28.21 @@ -234,7 +234,7 @@
   28.22      val ((f_binding, fT), mixfix) = the_single fixes;
   28.23      val fname = Binding.name_of f_binding;
   28.24  
   28.25 -    val cert = cterm_of (Proof_Context.theory_of lthy);
   28.26 +    val cert = Proof_Context.cterm_of lthy;
   28.27      val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop plain_eqn);
   28.28      val (head, args) = strip_comb lhs;
   28.29      val argnames = map (fst o dest_Free) args;
    29.1 --- a/src/HOL/Tools/Function/pat_completeness.ML	Tue Mar 03 17:20:51 2015 +0100
    29.2 +++ b/src/HOL/Tools/Function/pat_completeness.ML	Tue Mar 03 19:08:04 2015 +0100
    29.3 @@ -88,8 +88,8 @@
    29.4    then o_alg ctxt P idx vs
    29.5           (map (fn (pv :: pats, thm) =>
    29.6             (pats, refl RS
    29.7 -            (inst_free (cterm_of (Proof_Context.theory_of ctxt) pv)
    29.8 -              (cterm_of (Proof_Context.theory_of ctxt) v) thm))) pts)
    29.9 +            (inst_free (Proof_Context.cterm_of ctxt pv)
   29.10 +              (Proof_Context.cterm_of ctxt v) thm))) pts)
   29.11    else (* Cons case *)
   29.12      let
   29.13        val thy = Proof_Context.theory_of ctxt
    30.1 --- a/src/HOL/Tools/Function/relation.ML	Tue Mar 03 17:20:51 2015 +0100
    30.2 +++ b/src/HOL/Tools/Function/relation.ML	Tue Mar 03 19:08:04 2015 +0100
    30.3 @@ -33,7 +33,7 @@
    30.4    case Term.add_vars (prop_of st) [] of
    30.5      [v as (_, T)] =>
    30.6        let
    30.7 -        val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
    30.8 +        val cert = Proof_Context.cterm_of ctxt;
    30.9          val rel' = singleton (Variable.polymorphic ctxt) rel
   30.10            |> map_types Type_Infer.paramify_vars
   30.11            |> Type.constraint T
    31.1 --- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Tue Mar 03 17:20:51 2015 +0100
    31.2 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Tue Mar 03 19:08:04 2015 +0100
    31.3 @@ -23,7 +23,7 @@
    31.4      fun get_lhs thm = thm |> concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst
    31.5      val vars = get_lhs rel_Grp |> strip_comb |> snd |> map_filter (try (strip_comb #> snd #> hd))
    31.6      val UNIVs = map (fn var => HOLogic.mk_UNIV (var |> dest_Var |> snd |> dest_Type |> snd |> hd)) vars
    31.7 -    val inst = map2 (curry (apply2 (certify ctxt))) vars UNIVs
    31.8 +    val inst = map2 (curry (apply2 (Proof_Context.cterm_of ctxt))) vars UNIVs
    31.9      val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize ([], inst) 
   31.10        |> Local_Defs.unfold ctxt @{thms subset_UNIV[THEN eqTrueI] UNIV_def[symmetric] simp_thms(21)}
   31.11        |> (fn thm => thm RS sym)
    32.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Tue Mar 03 17:20:51 2015 +0100
    32.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue Mar 03 19:08:04 2015 +0100
    32.3 @@ -495,7 +495,7 @@
    32.4  in
    32.5  fun mk_readable_rsp_thm_eq tm lthy =
    32.6    let
    32.7 -    val ctm = cterm_of (Proof_Context.theory_of lthy) tm
    32.8 +    val ctm = Proof_Context.cterm_of lthy tm
    32.9      
   32.10      fun assms_rewr_conv tactic rule ct =
   32.11        let
   32.12 @@ -620,7 +620,7 @@
   32.13      val cr_to_pcr_conv = HOLogic.Trueprop_conv (Conv.fun2_conv 
   32.14        (Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy)))
   32.15      val (prsp_tm, rsp_prsp_eq) = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs)
   32.16 -      |> cterm_of (Proof_Context.theory_of lthy)
   32.17 +      |> Proof_Context.cterm_of lthy
   32.18        |> cr_to_pcr_conv
   32.19        |> ` concl_of
   32.20        |>> Logic.dest_equals
    33.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue Mar 03 17:20:51 2015 +0100
    33.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue Mar 03 19:08:04 2015 +0100
    33.3 @@ -352,7 +352,7 @@
    33.4  in  
    33.5    fun freeze_spec th ctxt =
    33.6      let
    33.7 -      val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
    33.8 +      val cert = Proof_Context.cterm_of ctxt;
    33.9        val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt;
   33.10        val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec;
   33.11      in (th RS spec', ctxt') end
    34.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Tue Mar 03 17:20:51 2015 +0100
    34.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Mar 03 19:08:04 2015 +0100
    34.3 @@ -694,7 +694,7 @@
    34.4  val (_, oracle) = Context.>>> (Context.map_theory_result
    34.5    (Thm.add_oracle (@{binding cooper},
    34.6      (fn (ctxt, t) =>
    34.7 -      (Thm.cterm_of (Proof_Context.theory_of ctxt) o Logic.mk_equals o apply2 HOLogic.mk_Trueprop)
    34.8 +      (Proof_Context.cterm_of ctxt o Logic.mk_equals o apply2 HOLogic.mk_Trueprop)
    34.9          (t, procedure t)))));
   34.10  
   34.11  val comp_ss =
    35.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Tue Mar 03 17:20:51 2015 +0100
    35.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Tue Mar 03 19:08:04 2015 +0100
    35.3 @@ -91,7 +91,7 @@
    35.4  
    35.5  fun mk_readable_rsp_thm_eq tm lthy =
    35.6    let
    35.7 -    val ctm = cterm_of (Proof_Context.theory_of lthy) tm
    35.8 +    val ctm = Proof_Context.cterm_of lthy tm
    35.9      
   35.10      fun norm_fun_eq ctm = 
   35.11        let
    36.1 --- a/src/HOL/Tools/SMT/smt_util.ML	Tue Mar 03 17:20:51 2015 +0100
    36.2 +++ b/src/HOL/Tools/SMT/smt_util.ML	Tue Mar 03 19:08:04 2015 +0100
    36.3 @@ -45,7 +45,6 @@
    36.4    val instT': cterm -> ctyp * cterm -> cterm
    36.5  
    36.6    (*certified terms*)
    36.7 -  val certify: Proof.context -> term -> cterm
    36.8    val typ_of: cterm -> typ
    36.9    val dest_cabs: cterm -> Proof.context -> cterm * Proof.context
   36.10    val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context
   36.11 @@ -180,8 +179,6 @@
   36.12  
   36.13  (* certified terms *)
   36.14  
   36.15 -fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt)
   36.16 -
   36.17  fun typ_of ct = #T (Thm.rep_cterm ct)
   36.18  
   36.19  fun dest_cabs ct ctxt =
    37.1 --- a/src/HOL/Tools/SMT/z3_replay.ML	Tue Mar 03 17:20:51 2015 +0100
    37.2 +++ b/src/HOL/Tools/SMT/z3_replay.ML	Tue Mar 03 19:08:04 2015 +0100
    37.3 @@ -23,7 +23,7 @@
    37.4      val maxidx = Thm.maxidx_of thm + 1
    37.5      val vs = params_of (Thm.prop_of thm)
    37.6      val vars = map_index (fn (i, (n, T)) => Var ((n, i + maxidx), T)) vs
    37.7 -  in Drule.forall_elim_list (map (SMT_Util.certify ctxt) vars) thm end
    37.8 +  in Drule.forall_elim_list (map (Proof_Context.cterm_of ctxt) vars) thm end
    37.9  
   37.10  fun add_paramTs names t =
   37.11    fold2 (fn n => fn (_, T) => AList.update (op =) (n, T)) names (params_of t)
   37.12 @@ -31,7 +31,7 @@
   37.13  fun new_fixes ctxt nTs =
   37.14    let
   37.15      val (ns, ctxt') = Variable.variant_fixes (replicate (length nTs) "") ctxt
   37.16 -    fun mk (n, T) n' = (n, SMT_Util.certify ctxt' (Free (n', T)))
   37.17 +    fun mk (n, T) n' = (n, Proof_Context.cterm_of ctxt' (Free (n', T)))
   37.18    in (ctxt', Symtab.make (map2 mk nTs ns)) end
   37.19  
   37.20  fun forall_elim_term ct (Const (@{const_name Pure.all}, _) $ (a as Abs _)) =
   37.21 @@ -60,7 +60,7 @@
   37.22    if Z3_Proof.is_assumption rule then
   37.23      (case Inttab.lookup assumed id of
   37.24        SOME (_, thm) => thm
   37.25 -    | NONE => Thm.assume (SMT_Util.certify ctxt concl))
   37.26 +    | NONE => Thm.assume (Proof_Context.cterm_of ctxt concl))
   37.27    else
   37.28      under_fixes (Z3_Replay_Methods.method_for rule) ctxt
   37.29        (if is_fix_step then (map snd nthms, []) else ([], nthms)) fixes concl
   37.30 @@ -123,7 +123,7 @@
   37.31          (cx as ((iidths, thms), (ctxt, ptab))) =
   37.32        if Z3_Proof.is_assumption rule andalso rule <> Z3_Proof.Hypothesis then
   37.33          let
   37.34 -          val ct = SMT_Util.certify ctxt concl
   37.35 +          val ct = Proof_Context.cterm_of ctxt concl
   37.36            val thm1 = Thm.trivial ct |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))
   37.37            val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1
   37.38          in
    38.1 --- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Tue Mar 03 17:20:51 2015 +0100
    38.2 +++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Tue Mar 03 19:08:04 2015 +0100
    38.3 @@ -88,7 +88,7 @@
    38.4  
    38.5  fun dest_thm thm = dest_prop (Thm.concl_of thm)
    38.6  
    38.7 -fun certify_prop ctxt t = SMT_Util.certify ctxt (as_prop t)
    38.8 +fun certify_prop ctxt t = Proof_Context.cterm_of ctxt (as_prop t)
    38.9  
   38.10  fun try_provers ctxt rule [] thms t = replay_rule_error ctxt rule thms t
   38.11    | try_provers ctxt rule ((name, prover) :: named_provers) thms t =
   38.12 @@ -108,13 +108,13 @@
   38.13  
   38.14  fun match_instantiateT ctxt t thm =
   38.15    if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then
   38.16 -    let val certT = Thm.ctyp_of (Proof_Context.theory_of ctxt)
   38.17 +    let val certT = Proof_Context.ctyp_of ctxt
   38.18      in Thm.instantiate (gen_certify_inst fst TVar certT ctxt thm t, []) thm end
   38.19    else thm
   38.20  
   38.21  fun match_instantiate ctxt t thm =
   38.22    let
   38.23 -    val cert = SMT_Util.certify ctxt
   38.24 +    val cert = Proof_Context.cterm_of ctxt
   38.25      val thm' = match_instantiateT ctxt t thm
   38.26    in Thm.instantiate ([], gen_certify_inst snd Var cert ctxt thm' t) thm' end
   38.27  
   38.28 @@ -402,7 +402,7 @@
   38.29    end
   38.30  
   38.31  fun forall_intr ctxt t thm =
   38.32 -  let val ct = Thm.cterm_of (Proof_Context.theory_of ctxt) t
   38.33 +  let val ct = Proof_Context.cterm_of ctxt t
   38.34    in Thm.forall_intr ct thm COMP_INCR @{thm iff_allI} end
   38.35  
   38.36  in
    39.1 --- a/src/HOL/Tools/TFL/post.ML	Tue Mar 03 17:20:51 2015 +0100
    39.2 +++ b/src/HOL/Tools/TFL/post.ML	Tue Mar 03 19:08:04 2015 +0100
    39.3 @@ -174,7 +174,7 @@
    39.4               (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
    39.5  in
    39.6  fun derive_init_eqs ctxt rules eqs =
    39.7 -  map (Thm.trivial o Thm.cterm_of (Proof_Context.theory_of ctxt) o HOLogic.mk_Trueprop) eqs
    39.8 +  map (Thm.trivial o Proof_Context.cterm_of ctxt o HOLogic.mk_Trueprop) eqs
    39.9    |> map_index (fn (i, e) => solve_eq ctxt (e, (get_related_thms i rules), i))
   39.10    |> flat;
   39.11  end;
    40.1 --- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Mar 03 17:20:51 2015 +0100
    40.2 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Mar 03 19:08:04 2015 +0100
    40.3 @@ -343,8 +343,8 @@
    40.4      val predTs = map mk_pred1T As
    40.5      val (preds, lthy) = mk_Frees "P" predTs lthy
    40.6      val args = map mk_eq_onp preds
    40.7 -    val cTs = map (SOME o certifyT lthy) (maps (replicate 2) As)
    40.8 -    val cts = map (SOME o certify lthy) args
    40.9 +    val cTs = map (SOME o Proof_Context.ctyp_of lthy) (maps (replicate 2) As)
   40.10 +    val cts = map (SOME o Proof_Context.cterm_of lthy) args
   40.11      fun get_rhs thm = thm |> concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
   40.12      fun is_eqn thm = can get_rhs thm
   40.13      fun rel2pred_massage thm =
    41.1 --- a/src/HOL/Tools/code_evaluation.ML	Tue Mar 03 17:20:51 2015 +0100
    41.2 +++ b/src/HOL/Tools/code_evaluation.ML	Tue Mar 03 19:08:04 2015 +0100
    41.3 @@ -204,7 +204,7 @@
    41.4  
    41.5  fun certify_eval ctxt value conv ct =
    41.6    let
    41.7 -    val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
    41.8 +    val cert = Proof_Context.cterm_of ctxt;
    41.9      val t = Thm.term_of ct;
   41.10      val T = fastype_of t;
   41.11      val mk_eq = Thm.mk_binop (cert (Const (@{const_name Pure.eq}, T --> T --> propT)));
    42.1 --- a/src/HOL/Tools/coinduction.ML	Tue Mar 03 17:20:51 2015 +0100
    42.2 +++ b/src/HOL/Tools/coinduction.ML	Tue Mar 03 19:08:04 2015 +0100
    42.3 @@ -79,7 +79,7 @@
    42.4              |> Ctr_Sugar_Util.list_exists_free vars
    42.5              |> Term.map_abs_vars (Variable.revert_fixed ctxt)
    42.6              |> fold_rev Term.absfree (names ~~ Ts)
    42.7 -            |> Ctr_Sugar_Util.certify ctxt;
    42.8 +            |> Proof_Context.cterm_of ctxt;
    42.9            val thm = Ctr_Sugar_Util.cterm_instantiate_pos [SOME phi] raw_thm;
   42.10            val e = length eqs;
   42.11            val p = length prems;
   42.12 @@ -88,7 +88,7 @@
   42.13              EVERY' (map (fn var =>
   42.14                resolve_tac ctxt
   42.15                  [Ctr_Sugar_Util.cterm_instantiate_pos
   42.16 -                  [NONE, SOME (Ctr_Sugar_Util.certify ctxt var)] exI]) vars),
   42.17 +                  [NONE, SOME (Proof_Context.cterm_of ctxt var)] exI]) vars),
   42.18              if p = 0 then Ctr_Sugar_Util.CONJ_WRAP' (K (resolve_tac ctxt [refl])) eqs
   42.19              else
   42.20                REPEAT_DETERM_N e o (resolve_tac ctxt [conjI] THEN' resolve_tac ctxt [refl]) THEN'
    43.1 --- a/src/HOL/Tools/inductive.ML	Tue Mar 03 17:20:51 2015 +0100
    43.2 +++ b/src/HOL/Tools/inductive.ML	Tue Mar 03 19:08:04 2015 +0100
    43.3 @@ -849,7 +849,7 @@
    43.4        ||> is_auxiliary ? Local_Theory.restore_naming lthy;
    43.5      val fp_def' =
    43.6        Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def])
    43.7 -        (cterm_of (Proof_Context.theory_of lthy') (list_comb (rec_const, params)));
    43.8 +        (Proof_Context.cterm_of lthy' (list_comb (rec_const, params)));
    43.9      val specs =
   43.10        if length cs < 2 then []
   43.11        else
    44.1 --- a/src/HOL/Tools/legacy_transfer.ML	Tue Mar 03 17:20:51 2015 +0100
    44.2 +++ b/src/HOL/Tools/legacy_transfer.ML	Tue Mar 03 19:08:04 2015 +0100
    44.3 @@ -59,9 +59,8 @@
    44.4  fun get_by_direction context (a, D) =
    44.5    let
    44.6      val ctxt = Context.proof_of context;
    44.7 -    val certify = Thm.cterm_of (Context.theory_of context);
    44.8 -    val a0 = certify a;
    44.9 -    val D0 = certify D;
   44.10 +    val a0 = Proof_Context.cterm_of ctxt a;
   44.11 +    val D0 = Proof_Context.cterm_of ctxt D;
   44.12      fun eq_direction ((a, D), thm') =
   44.13        let
   44.14          val (a', D') = direction_of thm';
   44.15 @@ -117,12 +116,11 @@
   44.16        |> Variable.declare_thm thm
   44.17        |> Variable.declare_term (term_of a)
   44.18        |> Variable.declare_term (term_of D);
   44.19 -    val certify = Thm.cterm_of (Proof_Context.theory_of ctxt3);
   44.20      val vars = filter (fn ((v, _), T) => Type.could_unify (T, aT) andalso
   44.21        not (member (op =) leave v)) (Term.add_vars (Thm.prop_of thm) []);
   44.22 -    val c_vars = map (certify o Var) vars;
   44.23 +    val c_vars = map (Proof_Context.cterm_of ctxt3 o Var) vars;
   44.24      val (vs', ctxt4) = Variable.variant_fixes (map (fst o fst) vars) ctxt3;
   44.25 -    val c_vars' = map (certify o (fn v => Free (v, bT))) vs';
   44.26 +    val c_vars' = map (Proof_Context.cterm_of ctxt3 o (fn v => Free (v, bT))) vs';
   44.27      val c_exprs' = map (Thm.apply a) c_vars';
   44.28  
   44.29      (* transfer *)
    45.1 --- a/src/HOL/Tools/reification.ML	Tue Mar 03 17:20:51 2015 +0100
    45.2 +++ b/src/HOL/Tools/reification.ML	Tue Mar 03 19:08:04 2015 +0100
    45.3 @@ -27,7 +27,7 @@
    45.4    let
    45.5      val ct = case some_t
    45.6       of NONE => Thm.dest_arg concl
    45.7 -      | SOME t => Thm.cterm_of (Proof_Context.theory_of ctxt) t
    45.8 +      | SOME t => Proof_Context.cterm_of ctxt t
    45.9      val thm = conv ct;
   45.10    in
   45.11      if Thm.is_reflexive thm then no_tac
   45.12 @@ -48,7 +48,7 @@
   45.13    let
   45.14      val Const (fN, _) = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
   45.15        |> fst |> strip_comb |> fst;
   45.16 -    val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
   45.17 +    val cert = Proof_Context.cterm_of ctxt;
   45.18      val ((_, [th']), ctxt') = Variable.import true [th] ctxt;
   45.19      val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'));
   45.20      fun add_fterms (t as t1 $ t2) =
   45.21 @@ -261,7 +261,7 @@
   45.22        |> fst)) eqs [];
   45.23      val tys = fold_rev (fn f => fold (insert (op =)) (f |> fastype_of |> binder_types |> tl)) fs [];
   45.24      val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt;
   45.25 -    val cert = cterm_of (Proof_Context.theory_of ctxt');
   45.26 +    val cert = Proof_Context.cterm_of ctxt';
   45.27      val subst =
   45.28        the o AList.lookup (op =) (map2 (fn T => fn v => (T, cert (Free (v, T)))) tys vs);
   45.29      fun prep_eq eq =
   45.30 @@ -285,7 +285,7 @@
   45.31        | is_list_var _ = false;
   45.32      val vars = th |> prop_of |> Logic.dest_equals |> snd
   45.33        |> strip_comb |> snd |> filter is_list_var;
   45.34 -    val cert = cterm_of (Proof_Context.theory_of ctxt);
   45.35 +    val cert = Proof_Context.cterm_of ctxt;
   45.36      val vs = map (fn v as Var (_, T) =>
   45.37        (v, the (AList.lookup Type.could_unify bds' T) |> snd |> HOLogic.mk_list (dest_listT T))) vars;
   45.38      val th' = Drule.instantiate_normalize ([], (map o apply2) cert vs) th;
    46.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Tue Mar 03 17:20:51 2015 +0100
    46.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Tue Mar 03 19:08:04 2015 +0100
    46.3 @@ -468,7 +468,7 @@
    46.4  fun conv ctxt t =
    46.5    let
    46.6      val ([t'], ctxt') = Variable.import_terms true [t] (Variable.declare_term t ctxt)
    46.7 -    val ct = cterm_of (Proof_Context.theory_of ctxt') t'
    46.8 +    val ct = Proof_Context.cterm_of ctxt' t'
    46.9      fun unfold_conv thms =
   46.10        Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
   46.11          (empty_simpset ctxt' addsimps thms)
   46.12 @@ -495,11 +495,10 @@
   46.13  
   46.14  fun instantiate_arg_cong ctxt pred =
   46.15    let
   46.16 -    val certify = cterm_of (Proof_Context.theory_of ctxt)
   46.17      val arg_cong = Thm.incr_indexes (maxidx_of_term pred + 1) @{thm arg_cong}
   46.18      val f $ _ = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (concl_of arg_cong)))
   46.19    in
   46.20 -    cterm_instantiate [(certify f, certify pred)] arg_cong
   46.21 +    cterm_instantiate [(Proof_Context.cterm_of ctxt f, Proof_Context.cterm_of ctxt pred)] arg_cong
   46.22    end;
   46.23  
   46.24  fun simproc ctxt redex =