clarified context;
authorwenzelm
Fri Mar 06 23:56:43 2015 +0100 (2015-03-06)
changeset 59642929984c529d3
parent 59641 a2d056424d3c
child 59643 f3be9235503d
clarified context;
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/Transfer/transfer.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/cnf.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/monomorph.ML
src/HOL/Tools/numeral.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Tools/record.ML
src/HOL/Tools/reification.ML
src/HOL/Tools/sat.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/hypsubst.ML
src/Tools/coherent.ML
src/Tools/cong_tac.ML
src/Tools/eqsubst.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Mar 06 23:55:55 2015 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Mar 06 23:56:43 2015 +0100
     1.3 @@ -469,7 +469,7 @@
     1.4        val T = mk_tupleT_balanced tfrees;
     1.5      in
     1.6        @{thm asm_rl[of "ALL x. P x --> Q x" for P Q]}
     1.7 -      |> Drule.instantiate' [SOME (Thm.global_ctyp_of @{theory} T)] []
     1.8 +      |> Drule.instantiate' [SOME (Thm.ctyp_of @{context} T)] []
     1.9        |> Raw_Simplifier.rewrite_goals_rule @{context} @{thms split_paired_All[THEN eq_reflection]}
    1.10        |> (fn thm => impI RS funpow n (fn th => allI RS th) thm)
    1.11        |> Thm.varifyT_global
     2.1 --- a/src/HOL/Tools/Transfer/transfer.ML	Fri Mar 06 23:55:55 2015 +0100
     2.2 +++ b/src/HOL/Tools/Transfer/transfer.ML	Fri Mar 06 23:56:43 2015 +0100
     2.3 @@ -222,7 +222,6 @@
     2.4  
     2.5  fun gen_abstract_equalities ctxt (dest : term -> term * (term -> term)) thm =
     2.6    let
     2.7 -    val thy = Thm.theory_of_thm thm
     2.8      val prop = Thm.prop_of thm
     2.9      val (t, mk_prop') = dest prop
    2.10      (* Only consider "op =" at non-base types *)
    2.11 @@ -238,7 +237,7 @@
    2.12      val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees
    2.13      val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
    2.14      val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
    2.15 -    val cprop = Thm.global_cterm_of thy prop2
    2.16 +    val cprop = Thm.cterm_of ctxt prop2
    2.17      val equal_thm = Raw_Simplifier.rewrite ctxt false [is_equality_lemma] cprop
    2.18      fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
    2.19    in
    2.20 @@ -317,7 +316,6 @@
    2.21  
    2.22  fun gen_abstract_domains ctxt (dest : term -> term * (term -> term)) thm =
    2.23    let
    2.24 -    val thy = Thm.theory_of_thm thm
    2.25      val prop = Thm.prop_of thm
    2.26      val (t, mk_prop') = dest prop
    2.27      val Domainp_tms = rev (fold_Domainp (fn t => insert op= t) t [])
    2.28 @@ -331,7 +329,7 @@
    2.29      val t' = subst_terms (fold Termtab.update (Domainp_tms ~~ frees) Termtab.empty) t
    2.30      val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
    2.31      val prop2 = Logic.list_rename_params (rev names) prop1
    2.32 -    val cprop = Thm.global_cterm_of thy prop2
    2.33 +    val cprop = Thm.cterm_of ctxt prop2
    2.34      val equal_thm = Raw_Simplifier.rewrite ctxt false [Domainp_lemma] cprop
    2.35      fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
    2.36    in
    2.37 @@ -415,60 +413,59 @@
    2.38  
    2.39  fun transfer_rule_of_terms (prj : typ * typ -> typ) ctxt tab t u =
    2.40    let
    2.41 -    val thy = Proof_Context.theory_of ctxt
    2.42      (* precondition: prj(T,U) must consist of only TFrees and type "fun" *)
    2.43      fun rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) =
    2.44 -        let
    2.45 -          val r1 = rel T1 U1
    2.46 -          val r2 = rel T2 U2
    2.47 -          val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U)
    2.48 -        in
    2.49 -          Const (@{const_name rel_fun}, rT) $ r1 $ r2
    2.50 -        end
    2.51 +          let
    2.52 +            val r1 = rel T1 U1
    2.53 +            val r2 = rel T2 U2
    2.54 +            val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U)
    2.55 +          in
    2.56 +            Const (@{const_name rel_fun}, rT) $ r1 $ r2
    2.57 +          end
    2.58        | rel T U =
    2.59 -        let
    2.60 -          val (a, _) = dest_TFree (prj (T, U))
    2.61 -        in
    2.62 -          Free (the (AList.lookup (op =) tab a), mk_relT (T, U))
    2.63 -        end
    2.64 +          let
    2.65 +            val (a, _) = dest_TFree (prj (T, U))
    2.66 +          in
    2.67 +            Free (the (AList.lookup (op =) tab a), mk_relT (T, U))
    2.68 +          end
    2.69      fun zip _ thms (Bound i) (Bound _) = (nth thms i, [])
    2.70        | zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) =
    2.71 -        let
    2.72 -          val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt
    2.73 -          val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U)
    2.74 -          val cprop = Thm.global_cterm_of thy (HOLogic.mk_Trueprop prop)
    2.75 -          val thm0 = Thm.assume cprop
    2.76 -          val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
    2.77 -          val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop))
    2.78 -          val r2 = Thm.dest_fun2 (Thm.dest_arg (Thm.cprop_of thm1))
    2.79 -          val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r1))
    2.80 -          val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r2))
    2.81 -          val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
    2.82 -          val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
    2.83 -          val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
    2.84 -          val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1))
    2.85 -        in
    2.86 -          (thm2 COMP rule, hyps)
    2.87 -        end
    2.88 +          let
    2.89 +            val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt
    2.90 +            val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U)
    2.91 +            val cprop = Thm.cterm_of ctxt' (HOLogic.mk_Trueprop prop)
    2.92 +            val thm0 = Thm.assume cprop
    2.93 +            val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
    2.94 +            val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop))
    2.95 +            val r2 = Thm.dest_fun2 (Thm.dest_arg (Thm.cprop_of thm1))
    2.96 +            val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r1))
    2.97 +            val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r2))
    2.98 +            val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
    2.99 +            val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
   2.100 +            val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
   2.101 +            val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1))
   2.102 +          in
   2.103 +            (thm2 COMP rule, hyps)
   2.104 +          end
   2.105        | zip ctxt thms (f $ t) (g $ u) =
   2.106 -        let
   2.107 -          val (thm1, hyps1) = zip ctxt thms f g
   2.108 -          val (thm2, hyps2) = zip ctxt thms t u
   2.109 -        in
   2.110 -          (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)
   2.111 -        end
   2.112 +          let
   2.113 +            val (thm1, hyps1) = zip ctxt thms f g
   2.114 +            val (thm2, hyps2) = zip ctxt thms t u
   2.115 +          in
   2.116 +            (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)
   2.117 +          end
   2.118        | zip _ _ t u =
   2.119 -        let
   2.120 -          val T = fastype_of t
   2.121 -          val U = fastype_of u
   2.122 -          val prop = mk_Rel (rel T U) $ t $ u
   2.123 -          val cprop = Thm.global_cterm_of thy (HOLogic.mk_Trueprop prop)
   2.124 -        in
   2.125 -          (Thm.assume cprop, [cprop])
   2.126 -        end
   2.127 +          let
   2.128 +            val T = fastype_of t
   2.129 +            val U = fastype_of u
   2.130 +            val prop = mk_Rel (rel T U) $ t $ u
   2.131 +            val cprop = Thm.cterm_of ctxt (HOLogic.mk_Trueprop prop)
   2.132 +          in
   2.133 +            (Thm.assume cprop, [cprop])
   2.134 +          end
   2.135      val r = mk_Rel (rel (fastype_of t) (fastype_of u))
   2.136      val goal = HOLogic.mk_Trueprop (r $ t $ u)
   2.137 -    val rename = Thm.trivial (Thm.global_cterm_of thy goal)
   2.138 +    val rename = Thm.trivial (Thm.cterm_of ctxt goal)
   2.139      val (thm, hyps) = zip ctxt [] t u
   2.140    in
   2.141      Drule.implies_intr_list hyps (thm RS rename)
   2.142 @@ -577,10 +574,8 @@
   2.143      val cbool = @{ctyp bool}
   2.144      val relT = @{typ "bool => bool => bool"}
   2.145      val idx = Thm.maxidx_of thm + 1
   2.146 -    val thy = Proof_Context.theory_of ctxt
   2.147 -    fun tinst (a, _) = (Thm.global_ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
   2.148 -    fun inst (a, t) =
   2.149 -      (Thm.global_cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), Thm.global_cterm_of thy t)
   2.150 +    fun tinst (a, _) = (Thm.ctyp_of ctxt' (TVar ((a, idx), @{sort type})), cbool)
   2.151 +    fun inst (a, t) = apply2 (Thm.cterm_of ctxt') (Var (Name.clean_index (prep a, idx), relT), t)
   2.152    in
   2.153      thm
   2.154        |> Thm.generalize (tfrees, rnames @ frees) idx
   2.155 @@ -603,10 +598,8 @@
   2.156      val cbool = @{ctyp bool}
   2.157      val relT = @{typ "bool => bool => bool"}
   2.158      val idx = Thm.maxidx_of thm + 1
   2.159 -    val thy = Proof_Context.theory_of ctxt
   2.160 -    fun tinst (a, _) = (Thm.global_ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
   2.161 -    fun inst (a, t) =
   2.162 -      (Thm.global_cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), Thm.global_cterm_of thy t)
   2.163 +    fun tinst (a, _) = (Thm.ctyp_of ctxt' (TVar ((a, idx), @{sort type})), cbool)
   2.164 +    fun inst (a, t) = apply2 (Thm.cterm_of ctxt') (Var (Name.clean_index (prep a, idx), relT), t)
   2.165    in
   2.166      thm
   2.167        |> Thm.generalize (tfrees, rnames @ frees) idx
     3.1 --- a/src/HOL/Tools/choice_specification.ML	Fri Mar 06 23:55:55 2015 +0100
     3.2 +++ b/src/HOL/Tools/choice_specification.ML	Fri Mar 06 23:56:43 2015 +0100
     3.3 @@ -83,7 +83,7 @@
     3.4      val ctxt = Proof_Context.init_global thy
     3.5  
     3.6      val rew_imps = alt_props |>
     3.7 -      map (Object_Logic.atomize ctxt o Thm.global_cterm_of thy o Syntax.read_prop_global thy o snd)
     3.8 +      map (Object_Logic.atomize ctxt o Thm.cterm_of ctxt o Syntax.read_prop_global thy o snd)
     3.9      val props' = rew_imps |>
    3.10        map (HOLogic.dest_Trueprop o Thm.term_of o snd o Thm.dest_equals o Thm.cprop_of)
    3.11  
     4.1 --- a/src/HOL/Tools/cnf.ML	Fri Mar 06 23:55:55 2015 +0100
     4.2 +++ b/src/HOL/Tools/cnf.ML	Fri Mar 06 23:56:43 2015 +0100
     4.3 @@ -259,14 +259,13 @@
     4.4  
     4.5  fun make_under_quantifiers ctxt make t =
     4.6    let
     4.7 -    val thy = Proof_Context.theory_of ctxt
     4.8      fun conv ctxt ct =
     4.9        (case Thm.term_of ct of
    4.10          Const _ $ Abs _ => Conv.comb_conv (conv ctxt) ct
    4.11        | Abs _ => Conv.abs_conv (conv o snd) ctxt ct
    4.12        | Const _ => Conv.all_conv ct
    4.13        | t => make t RS eq_reflection)
    4.14 -  in conv ctxt (Thm.global_cterm_of thy t) RS meta_eq_to_obj_eq end
    4.15 +  in conv ctxt (Thm.cterm_of ctxt t) RS meta_eq_to_obj_eq end
    4.16  
    4.17  fun make_nnf_thm_under_quantifiers ctxt =
    4.18    make_under_quantifiers ctxt (make_nnf_thm (Proof_Context.theory_of ctxt))
     5.1 --- a/src/HOL/Tools/datatype_realizer.ML	Fri Mar 06 23:55:55 2015 +0100
     5.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Fri Mar 06 23:56:43 2015 +0100
     5.3 @@ -105,11 +105,11 @@
     5.4          (map (fn ((((i, _), T), U), tname) =>
     5.5            make_pred i U T (mk_proj i is r) (Free (tname, T)))
     5.6              (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
     5.7 -    val inst = map (apply2 (Thm.global_cterm_of thy)) (map head_of (HOLogic.dest_conj
     5.8 +    val inst = map (apply2 (Thm.cterm_of ctxt)) (map head_of (HOLogic.dest_conj
     5.9        (HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~ ps);
    5.10  
    5.11      val thm =
    5.12 -      Goal.prove_internal ctxt (map (Thm.global_cterm_of thy) prems) (Thm.global_cterm_of thy concl)
    5.13 +      Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems) (Thm.cterm_of ctxt concl)
    5.14          (fn prems =>
    5.15             EVERY [
    5.16              rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
    5.17 @@ -185,12 +185,12 @@
    5.18      val y' = Free ("y", T);
    5.19  
    5.20      val thm =
    5.21 -      Goal.prove_internal ctxt (map (Thm.global_cterm_of thy) prems)
    5.22 -        (Thm.global_cterm_of thy
    5.23 +      Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems)
    5.24 +        (Thm.cterm_of ctxt
    5.25            (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
    5.26          (fn prems =>
    5.27             EVERY [
    5.28 -            rtac (cterm_instantiate [apply2 (Thm.global_cterm_of thy) (y, y')] exhaust) 1,
    5.29 +            rtac (cterm_instantiate [apply2 (Thm.cterm_of ctxt) (y, y')] exhaust) 1,
    5.30              ALLGOALS (EVERY'
    5.31                [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
    5.32                 resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])
     6.1 --- a/src/HOL/Tools/inductive.ML	Fri Mar 06 23:55:55 2015 +0100
     6.2 +++ b/src/HOL/Tools/inductive.ML	Fri Mar 06 23:56:43 2015 +0100
     6.3 @@ -565,15 +565,13 @@
     6.4  
     6.5  fun mk_cases ctxt prop =
     6.6    let
     6.7 -    val thy = Proof_Context.theory_of ctxt;
     6.8 -
     6.9      fun err msg =
    6.10        error (Pretty.string_of (Pretty.block
    6.11          [Pretty.str msg, Pretty.fbrk, Syntax.pretty_term ctxt prop]));
    6.12  
    6.13      val elims = Induct.find_casesP ctxt prop;
    6.14  
    6.15 -    val cprop = Thm.global_cterm_of thy prop;
    6.16 +    val cprop = Thm.cterm_of ctxt prop;
    6.17      fun mk_elim rl =
    6.18        Thm.implies_intr cprop
    6.19          (Tactic.rule_by_tactic ctxt (mk_cases_tac ctxt) (Thm.assume cprop RS rl))
    6.20 @@ -636,7 +634,7 @@
    6.21        | _ => error
    6.22          ("equations matching pattern " ^ Syntax.string_of_term ctxt prop ^ " is not unique"));
    6.23      val inst =
    6.24 -      map (fn v => (Thm.global_cterm_of thy (Var v), Thm.global_cterm_of thy (Envir.subst_term subst (Var v))))
    6.25 +      map (fn v => apply2 (Thm.cterm_of ctxt') (Var v, Envir.subst_term subst (Var v)))
    6.26          (Term.add_vars (lhs_of eq) []);
    6.27    in
    6.28      Drule.cterm_instantiate inst eq
     7.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Mar 06 23:55:55 2015 +0100
     7.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri Mar 06 23:56:43 2015 +0100
     7.3 @@ -41,10 +41,9 @@
     7.4  fun strong_ind_simproc tab =
     7.5    Simplifier.simproc_global_i @{theory HOL} "strong_ind" [anyt] (fn ctxt => fn t =>
     7.6      let
     7.7 -      val thy = Proof_Context.theory_of ctxt;
     7.8        fun close p t f =
     7.9          let val vs = Term.add_vars t []
    7.10 -        in Drule.instantiate' [] (rev (map (SOME o Thm.global_cterm_of thy o Var) vs))
    7.11 +        in Drule.instantiate' [] (rev (map (SOME o Thm.cterm_of ctxt o Var) vs))
    7.12            (p (fold (Logic.all o Var) vs t) f)
    7.13          end;
    7.14        fun mkop @{const_name HOL.conj} T x =
    7.15 @@ -93,8 +92,8 @@
    7.16              in
    7.17                if forall is_none rews then NONE
    7.18                else SOME (fold (fn th1 => fn th2 => Thm.combination th2 th1)
    7.19 -                (map2 (fn SOME r => K r | NONE => Thm.reflexive o Thm.global_cterm_of thy)
    7.20 -                   rews ts) (Thm.reflexive (Thm.global_cterm_of thy h)))
    7.21 +                (map2 (fn SOME r => K r | NONE => Thm.reflexive o Thm.cterm_of ctxt)
    7.22 +                   rews ts) (Thm.reflexive (Thm.cterm_of ctxt h)))
    7.23              end
    7.24          | NONE => NONE)
    7.25        | _ => NONE
    7.26 @@ -200,7 +199,7 @@
    7.27  (* 3. simplify                                                *)
    7.28  (**************************************************************)
    7.29  
    7.30 -fun mk_to_pred_inst thy fs =
    7.31 +fun mk_to_pred_inst ctxt fs =
    7.32    map (fn (x, ps) =>
    7.33      let
    7.34        val (Ts, T) = strip_type (fastype_of x);
    7.35 @@ -208,8 +207,8 @@
    7.36        val x' = map_type
    7.37          (K (Ts @ HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x;
    7.38      in
    7.39 -      (Thm.global_cterm_of thy x,
    7.40 -       Thm.global_cterm_of thy (fold_rev (Term.abs o pair "x") Ts
    7.41 +      (Thm.cterm_of ctxt x,
    7.42 +       Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts
    7.43           (HOLogic.Collect_const U $
    7.44              HOLogic.mk_psplits ps U HOLogic.boolT
    7.45                (list_comb (x', map Bound (length Ts - 1 downto 0))))))
    7.46 @@ -217,8 +216,7 @@
    7.47  
    7.48  fun mk_to_pred_eq ctxt p fs optfs' T thm =
    7.49    let
    7.50 -    val thy = Thm.theory_of_thm thm;
    7.51 -    val insts = mk_to_pred_inst thy fs;
    7.52 +    val insts = mk_to_pred_inst ctxt fs;
    7.53      val thm' = Thm.instantiate ([], insts) thm;
    7.54      val thm'' =
    7.55        (case optfs' of
    7.56 @@ -233,7 +231,7 @@
    7.57                Thm.dest_comb |> snd |> Drule.strip_comb |> snd |> hd |> Thm.dest_comb
    7.58            in
    7.59              thm' RS (Drule.cterm_instantiate [(arg_cong_f,
    7.60 -              Thm.global_cterm_of thy (Abs ("P", Ts ---> HOLogic.boolT,
    7.61 +              Thm.cterm_of ctxt (Abs ("P", Ts ---> HOLogic.boolT,
    7.62                  HOLogic.Collect_const U $ HOLogic.mk_psplits fs' U
    7.63                    HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
    7.64            end)
    7.65 @@ -322,7 +320,8 @@
    7.66          lookup_rule (Proof_Context.theory_of ctxt) (Thm.prop_of #> Logic.dest_equals) rules')
    7.67    end;
    7.68  
    7.69 -fun to_pred_proc thy rules t = case lookup_rule thy I rules t of
    7.70 +fun to_pred_proc thy rules t =
    7.71 +  case lookup_rule thy I rules t of
    7.72      NONE => NONE
    7.73    | SOME (lhs, rhs) =>
    7.74        SOME (Envir.subst_term
    7.75 @@ -337,7 +336,7 @@
    7.76      val fs = filter (is_Var o fst)
    7.77        (infer_arities thy set_arities (NONE, Thm.prop_of thm) []);
    7.78      (* instantiate each set parameter with {(x, y). p x y} *)
    7.79 -    val insts = mk_to_pred_inst thy fs
    7.80 +    val insts = mk_to_pred_inst ctxt fs
    7.81    in
    7.82      thm |>
    7.83      Thm.instantiate ([], insts) |>
    7.84 @@ -370,8 +369,8 @@
    7.85          val T = HOLogic.mk_ptupleT ps Us;
    7.86          val x' = map_type (K (Rs ---> HOLogic.mk_setT T)) x
    7.87        in
    7.88 -        (Thm.global_cterm_of thy x,
    7.89 -         Thm.global_cterm_of thy (fold_rev (Term.abs o pair "x") Ts
    7.90 +        (Thm.cterm_of ctxt x,
    7.91 +         Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts
    7.92            (HOLogic.mk_mem (HOLogic.mk_ptuple ps T (map Bound (k downto 0)),
    7.93               list_comb (x', map Bound (l - 1 downto k + 1))))))
    7.94        end) fs;
     8.1 --- a/src/HOL/Tools/monomorph.ML	Fri Mar 06 23:55:55 2015 +0100
     8.2 +++ b/src/HOL/Tools/monomorph.ML	Fri Mar 06 23:56:43 2015 +0100
     8.3 @@ -157,9 +157,9 @@
     8.4  
     8.5  (* collecting instances *)
     8.6  
     8.7 -fun instantiate thy subst =
     8.8 +fun instantiate ctxt subst =
     8.9    let
    8.10 -    fun cert (ix, (S, T)) = apply2 (Thm.global_ctyp_of thy) (TVar (ix, S), T)
    8.11 +    fun cert (ix, (S, T)) = apply2 (Thm.ctyp_of ctxt) (TVar (ix, S), T)
    8.12      fun cert' subst = Vartab.fold (cons o cert) subst []
    8.13    in Thm.instantiate (cert' subst, []) end
    8.14  
    8.15 @@ -186,7 +186,7 @@
    8.16          raise ENOUGH cx
    8.17        else
    8.18          let
    8.19 -          val thm' = instantiate thy subst thm
    8.20 +          val thm' = instantiate ctxt subst thm
    8.21            val rthm = ((round, subst), thm')
    8.22            val rthms = Inttab.lookup_list insts id;
    8.23            val n_insts' =
     9.1 --- a/src/HOL/Tools/numeral.ML	Fri Mar 06 23:55:55 2015 +0100
     9.2 +++ b/src/HOL/Tools/numeral.ML	Fri Mar 06 23:56:43 2015 +0100
     9.3 @@ -44,10 +44,10 @@
     9.4  val oneT = Thm.ctyp_of_cterm one;
     9.5  
     9.6  val numeral = @{cpat "numeral"};
     9.7 -val numeralT = Thm.global_ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm numeral));
     9.8 +val numeralT = Thm.ctyp_of @{context} (Term.range_type (Thm.typ_of_cterm numeral));
     9.9  
    9.10  val uminus = @{cpat "uminus"};
    9.11 -val uminusT = Thm.global_ctyp_of @{theory} (Term.range_type (Thm.typ_of_cterm uminus));
    9.12 +val uminusT = Thm.ctyp_of @{context} (Term.range_type (Thm.typ_of_cterm uminus));
    9.13  
    9.14  fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
    9.15  
    10.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Fri Mar 06 23:55:55 2015 +0100
    10.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Fri Mar 06 23:56:43 2015 +0100
    10.3 @@ -483,7 +483,7 @@
    10.4      simplify_one ctxt (([th, cancel_th]) MRS trans);
    10.5  
    10.6  local
    10.7 -  val Tp_Eq = Thm.reflexive (Thm.global_cterm_of @{theory HOL} HOLogic.Trueprop)
    10.8 +  val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory_context HOL} HOLogic.Trueprop)
    10.9    fun Eq_True_elim Eq = 
   10.10      Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
   10.11  in
   10.12 @@ -492,9 +492,8 @@
   10.13        val zero = Const(@{const_name Groups.zero}, T);
   10.14        val less = Const(@{const_name Orderings.less}, [T,T] ---> HOLogic.boolT);
   10.15        val pos = less $ zero $ t and neg = less $ t $ zero
   10.16 -      val thy = Proof_Context.theory_of ctxt
   10.17        fun prove p =
   10.18 -        SOME (Eq_True_elim (Simplifier.asm_rewrite ctxt (Thm.global_cterm_of thy p)))
   10.19 +        SOME (Eq_True_elim (Simplifier.asm_rewrite ctxt (Thm.cterm_of ctxt p)))
   10.20          handle THM _ => NONE
   10.21      in case prove pos of
   10.22           SOME th => SOME(th RS pos_th)
    11.1 --- a/src/HOL/Tools/record.ML	Fri Mar 06 23:55:55 2015 +0100
    11.2 +++ b/src/HOL/Tools/record.ML	Fri Mar 06 23:56:43 2015 +0100
    11.3 @@ -1375,9 +1375,9 @@
    11.4  
    11.5      fun mk_split_free_tac free induct_thm i =
    11.6        let
    11.7 -        val cfree = Thm.global_cterm_of thy free;
    11.8 +        val cfree = Thm.cterm_of ctxt free;
    11.9          val _$ (_ $ r) = Thm.concl_of induct_thm;
   11.10 -        val crec = Thm.global_cterm_of thy r;
   11.11 +        val crec = Thm.cterm_of ctxt r;
   11.12          val thm = cterm_instantiate [(crec, cfree)] induct_thm;
   11.13        in
   11.14          simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms induct_atomize}) i THEN
   11.15 @@ -1606,7 +1606,7 @@
   11.16        (roughly) the definition of the accessor.*)
   11.17      val surject = timeit_msg ctxt "record extension surjective proof:" (fn () =>
   11.18        let
   11.19 -        val cterm_ext = Thm.global_cterm_of defs_thy ext;
   11.20 +        val cterm_ext = Thm.cterm_of defs_ctxt ext;
   11.21          val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
   11.22          val tactic1 =
   11.23            simp_tac (put_simpset HOL_basic_ss defs_ctxt addsimps [ext_def]) 1 THEN
   11.24 @@ -1943,8 +1943,8 @@
   11.25                fun to_Var (Free (c, T)) = Var ((c, 1), T);
   11.26              in mk_rec (map to_Var all_vars_more) 0 end;
   11.27  
   11.28 -          val cterm_rec = Thm.global_cterm_of ext_thy r_rec0;
   11.29 -          val cterm_vrs = Thm.global_cterm_of ext_thy r_rec0_Vars;
   11.30 +          val cterm_rec = Thm.cterm_of ext_ctxt r_rec0;
   11.31 +          val cterm_vrs = Thm.cterm_of ext_ctxt r_rec0_Vars;
   11.32            val insts = [("v", cterm_rec), ("v'", cterm_vrs)];
   11.33            val init_thm = named_cterm_instantiate insts updacc_eq_triv;
   11.34            val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
    12.1 --- a/src/HOL/Tools/reification.ML	Fri Mar 06 23:55:55 2015 +0100
    12.2 +++ b/src/HOL/Tools/reification.ML	Fri Mar 06 23:56:43 2015 +0100
    12.3 @@ -169,12 +169,12 @@
    12.4            val (fnvs, invs) = List.partition (fn ((vn, _),_) => member (op =) vns vn) (Vartab.dest tmenv);
    12.5            val (fts, its) =
    12.6              (map (snd o snd) fnvs,
    12.7 -             map (fn ((vn, vi), (tT, t)) => apply2 (Thm.global_cterm_of thy) (Var ((vn, vi), tT), t)) invs);
    12.8 +             map (fn ((vn, vi), (tT, t)) => apply2 (Thm.cterm_of ctxt) (Var ((vn, vi), tT), t)) invs);
    12.9            val ctyenv =
   12.10 -            map (fn ((vn, vi), (s, ty)) => apply2 (Thm.global_ctyp_of thy) (TVar ((vn, vi), s), ty))
   12.11 +            map (fn ((vn, vi), (s, ty)) => apply2 (Thm.ctyp_of ctxt) (TVar ((vn, vi), s), ty))
   12.12                (Vartab.dest tyenv);
   12.13          in
   12.14 -          ((map (Thm.global_cterm_of thy) fts ~~ replicate (length fts) ctxt,
   12.15 +          ((map (Thm.cterm_of ctxt) fts ~~ replicate (length fts) ctxt,
   12.16               apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds)
   12.17          end handle Pattern.MATCH => decomp_reify da congs (ct, ctxt) bds))
   12.18    end;
   12.19 @@ -203,14 +203,14 @@
   12.20          val sbst = Envir.subst_term (tyenv, tmenv);
   12.21          val sbsT = Envir.subst_type tyenv;
   12.22          val subst_ty =
   12.23 -          map (fn (n, (s, t)) => apply2 (Thm.global_ctyp_of thy) (TVar (n, s), t)) (Vartab.dest tyenv)
   12.24 +          map (fn (n, (s, t)) => apply2 (Thm.ctyp_of ctxt'') (TVar (n, s), t)) (Vartab.dest tyenv)
   12.25          val tml = Vartab.dest tmenv;
   12.26          val (subst_ns, bds) = fold_map
   12.27            (fn (Const _ $ _ $ n, Var (xn0, _)) => fn bds =>
   12.28              let
   12.29                val name = snd (the (AList.lookup (op =) tml xn0));
   12.30                val (idx, bds) = index_of name bds;
   12.31 -            in (apply2 (Thm.global_cterm_of thy) (n, idx |> HOLogic.mk_nat), bds) end) subst bds;
   12.32 +            in (apply2 (Thm.cterm_of ctxt'') (n, idx |> HOLogic.mk_nat), bds) end) subst bds;
   12.33          val subst_vs =
   12.34            let
   12.35              fun h (Const _ $ (vs as Var (_, lT)) $ _, Var (_, T)) =
   12.36 @@ -220,10 +220,10 @@
   12.37                  val (bsT, _) = the (AList.lookup Type.could_unify bds lT);
   12.38                  val vsn = the (AList.lookup (op =) vsns_map vs);
   12.39                  val vs' = fold_rev (fn x => fn xs => cns $ x $xs) bsT (Free (vsn, lT'));
   12.40 -              in apply2 (Thm.global_cterm_of thy) (vs, vs') end;
   12.41 +              in apply2 (Thm.cterm_of ctxt'') (vs, vs') end;
   12.42            in map h subst end;
   12.43          val cts =
   12.44 -          map (fn ((vn, vi), (tT, t)) => apply2 (Thm.global_cterm_of thy) (Var ((vn, vi), tT), t))
   12.45 +          map (fn ((vn, vi), (tT, t)) => apply2 (Thm.cterm_of ctxt'') (Var ((vn, vi), tT), t))
   12.46              (fold (AList.delete (fn (((a : string), _), (b, _)) => a = b))
   12.47                (map (fn n => (n, 0)) xns) tml);
   12.48          val substt =
    13.1 --- a/src/HOL/Tools/sat.ML	Fri Mar 06 23:55:55 2015 +0100
    13.2 +++ b/src/HOL/Tools/sat.ML	Fri Mar 06 23:56:43 2015 +0100
    13.3 @@ -73,7 +73,7 @@
    13.4  val resolution_thm =
    13.5    @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
    13.6  
    13.7 -val cP = Thm.global_cterm_of @{theory} (Var (("P", 0), HOLogic.boolT));
    13.8 +val cP = Thm.cterm_of @{context} (Var (("P", 0), HOLogic.boolT));
    13.9  
   13.10  (* ------------------------------------------------------------------------- *)
   13.11  (* lit_ord: an order on integers that considers their absolute values only,  *)
    14.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Fri Mar 06 23:55:55 2015 +0100
    14.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Mar 06 23:56:43 2015 +0100
    14.3 @@ -903,9 +903,8 @@
    14.4  
    14.5  fun prover ctxt thms Tconcl (js : injust list) split_neq pos : thm option =
    14.6    let
    14.7 -    val thy = Proof_Context.theory_of ctxt
    14.8      val nTconcl = LA_Logic.neg_prop Tconcl
    14.9 -    val cnTconcl = Thm.global_cterm_of thy nTconcl
   14.10 +    val cnTconcl = Thm.cterm_of ctxt nTconcl
   14.11      val nTconclthm = Thm.assume cnTconcl
   14.12      val tree = (if split_neq then splitasms ctxt else Tip) (thms @ [nTconclthm])
   14.13      val (Falsethm, _) = fwdproof ctxt tree js
    15.1 --- a/src/Provers/hypsubst.ML	Fri Mar 06 23:55:55 2015 +0100
    15.2 +++ b/src/Provers/hypsubst.ML	Fri Mar 06 23:56:43 2015 +0100
    15.3 @@ -168,7 +168,6 @@
    15.4        Data.dest_Trueprop #> Data.dest_eq #> apply2 contract) (Thm.term_of cBi) of
    15.5      SOME (t, t') =>
    15.6        let
    15.7 -        val thy = Proof_Context.theory_of ctxt;
    15.8          val Bi = Thm.term_of cBi;
    15.9          val ps = Logic.strip_params Bi;
   15.10          val U = Term.fastype_of1 (rev (map snd ps), t);
   15.11 @@ -184,10 +183,10 @@
   15.12              (case (if b then t else t') of
   15.13                Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
   15.14              | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
   15.15 -        val (instT, _) = Thm.match (apply2 (Thm.global_cterm_of thy o Logic.mk_type) (V, U));
   15.16 +        val (instT, _) = Thm.match (apply2 (Thm.cterm_of ctxt o Logic.mk_type) (V, U));
   15.17        in
   15.18          compose_tac ctxt (true, Drule.instantiate_normalize (instT,
   15.19 -          map (apply2 (Thm.global_cterm_of thy))
   15.20 +          map (apply2 (Thm.cterm_of ctxt))
   15.21              [(Var (ixn, Ts ---> U --> body_type T), u),
   15.22               (Var (fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
   15.23               (Var (fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl',
    16.1 --- a/src/Tools/coherent.ML	Fri Mar 06 23:55:55 2015 +0100
    16.2 +++ b/src/Tools/coherent.ML	Fri Mar 06 23:56:43 2015 +0100
    16.3 @@ -173,19 +173,16 @@
    16.4  
    16.5  fun thm_of_cl_prf ctxt goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
    16.6    let
    16.7 -    val thy = Proof_Context.theory_of ctxt;
    16.8 -    val cert = Thm.global_cterm_of thy;
    16.9 -    val certT = Thm.global_ctyp_of thy;
   16.10      val _ =
   16.11        cond_trace ctxt (fn () =>
   16.12          Pretty.string_of (Pretty.big_list "asms:" (map (Display.pretty_thm ctxt) asms)));
   16.13      val th' =
   16.14        Drule.implies_elim_list
   16.15          (Thm.instantiate
   16.16 -           (map (fn (ixn, (S, T)) => (certT (TVar ((ixn, S))), certT T)) (Vartab.dest tye),
   16.17 +           (map (fn (ixn, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (ixn, S), T)) (Vartab.dest tye),
   16.18              map (fn (ixn, (T, t)) =>
   16.19 -              (cert (Var (ixn, Envir.subst_type tye T)), cert t)) (Vartab.dest env) @
   16.20 -            map (fn (ixnT, t) => (cert (Var ixnT), cert t)) insts) th)
   16.21 +              apply2 (Thm.cterm_of ctxt) (Var (ixn, Envir.subst_type tye T), t)) (Vartab.dest env) @
   16.22 +            map (fn (ixnT, t) => apply2 (Thm.cterm_of ctxt) (Var ixnT, t)) insts) th)
   16.23          (map (nth asms) is);
   16.24      val (_, cases) = dest_elim (Thm.prop_of th');
   16.25    in
   16.26 @@ -201,10 +198,8 @@
   16.27  
   16.28  and thm_of_case_prf ctxt goal asms ((params, prf), (_, asms')) =
   16.29    let
   16.30 -    val thy = Proof_Context.theory_of ctxt;
   16.31 -    val cert = Thm.global_cterm_of thy;
   16.32 -    val cparams = map cert params;
   16.33 -    val asms'' = map (cert o curry subst_bounds (rev params)) asms';
   16.34 +    val cparams = map (Thm.cterm_of ctxt) params;
   16.35 +    val asms'' = map (Thm.cterm_of ctxt o curry subst_bounds (rev params)) asms';
   16.36      val (prems'', ctxt') = fold_map Thm.assume_hyps asms'' ctxt;
   16.37    in
   16.38      Drule.forall_intr_list cparams
    17.1 --- a/src/Tools/cong_tac.ML	Fri Mar 06 23:55:55 2015 +0100
    17.2 +++ b/src/Tools/cong_tac.ML	Fri Mar 06 23:56:43 2015 +0100
    17.3 @@ -14,7 +14,6 @@
    17.4  
    17.5  fun cong_tac ctxt cong = CSUBGOAL (fn (cgoal, i) =>
    17.6    let
    17.7 -    val cert = Thm.global_cterm_of (Thm.theory_of_cterm cgoal);
    17.8      val goal = Thm.term_of cgoal;
    17.9    in
   17.10      (case Logic.strip_assums_concl goal of
   17.11 @@ -25,7 +24,7 @@
   17.12            val ps = Logic.strip_params (Thm.concl_of cong');
   17.13            val insts =
   17.14              [(f', f), (g', g), (x', x), (y', y)]
   17.15 -            |> map (fn (t, u) => (cert (Term.head_of t), cert (fold_rev Term.abs ps u)));
   17.16 +            |> map (fn (t, u) => apply2 (Thm.cterm_of ctxt) (Term.head_of t, fold_rev Term.abs ps u));
   17.17          in
   17.18            fn st =>
   17.19              compose_tac ctxt (false, Drule.cterm_instantiate insts cong', 2) i st
    18.1 --- a/src/Tools/eqsubst.ML	Fri Mar 06 23:55:55 2015 +0100
    18.2 +++ b/src/Tools/eqsubst.ML	Fri Mar 06 23:56:43 2015 +0100
    18.3 @@ -259,14 +259,11 @@
    18.4      val th = Thm.incr_indexes 1 gth;
    18.5      val tgt_term = Thm.prop_of th;
    18.6  
    18.7 -    val thy = Thm.theory_of_thm th;
    18.8 -    val cert = Thm.global_cterm_of thy;
    18.9 -
   18.10      val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
   18.11 -    val cfvs = rev (map cert fvs);
   18.12 +    val cfvs = rev (map (Thm.cterm_of ctxt) fvs);
   18.13  
   18.14      val conclterm = Logic.strip_imp_concl fixedbody;
   18.15 -    val conclthm = Thm.trivial (cert conclterm);
   18.16 +    val conclthm = Thm.trivial (Thm.cterm_of ctxt conclterm);
   18.17      val maxidx = Thm.maxidx_of th;
   18.18      val ft =
   18.19        (Zipper.move_down_right (* ==> *)
   18.20 @@ -274,7 +271,7 @@
   18.21         o Zipper.mktop
   18.22         o Thm.prop_of) conclthm
   18.23    in
   18.24 -    ((cfvs, conclthm), (thy, maxidx, ft))
   18.25 +    ((cfvs, conclthm), (Proof_Context.theory_of ctxt, maxidx, ft))
   18.26    end;
   18.27  
   18.28  (* substitute using an object or meta level equality *)
    19.1 --- a/src/Tools/nbe.ML	Fri Mar 06 23:55:55 2015 +0100
    19.2 +++ b/src/Tools/nbe.ML	Fri Mar 06 23:56:43 2015 +0100
    19.3 @@ -580,10 +580,9 @@
    19.4  
    19.5  fun mk_equals ctxt lhs raw_rhs =
    19.6    let
    19.7 -    val thy = Proof_Context.theory_of ctxt;
    19.8      val ty = Thm.typ_of_cterm lhs;
    19.9 -    val eq = Thm.global_cterm_of thy (Term.Const (@{const_name Pure.eq}, ty --> ty --> propT));
   19.10 -    val rhs = Thm.global_cterm_of thy raw_rhs;
   19.11 +    val eq = Thm.cterm_of ctxt (Term.Const (@{const_name Pure.eq}, ty --> ty --> propT));
   19.12 +    val rhs = Thm.cterm_of ctxt raw_rhs;
   19.13    in Thm.mk_binop eq lhs rhs end;
   19.14  
   19.15  val (_, raw_oracle) = Context.>>> (Context.map_theory_result