clarified context;
authorwenzelm
Fri Mar 06 23:44:57 2015 +0100 (2015-03-06)
changeset 596325980e75a204e
parent 59631 34030d67afb9
child 59633 a372513af1e2
clarified context;
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/ATP/atp_util.ML
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smt_real.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/SMT/smt_util.ML
src/HOL/Tools/SMT/z3_interface.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Mar 06 23:44:51 2015 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Mar 06 23:44:57 2015 +0100
     1.3 @@ -758,13 +758,11 @@
     1.4                      (0 upto length Ts - 1 ~~ Ts))
     1.5  
     1.6  fun do_introduce_combinators ctxt Ts t =
     1.7 -  let val thy = Proof_Context.theory_of ctxt in
     1.8 -    t |> conceal_bounds Ts
     1.9 -      |> Thm.global_cterm_of thy
    1.10 -      |> Meson_Clausify.introduce_combinators_in_cterm
    1.11 -      |> Thm.prop_of |> Logic.dest_equals |> snd
    1.12 -      |> reveal_bounds Ts
    1.13 -  end
    1.14 +  (t |> conceal_bounds Ts
    1.15 +     |> Thm.cterm_of ctxt
    1.16 +     |> Meson_Clausify.introduce_combinators_in_cterm
    1.17 +     |> Thm.prop_of |> Logic.dest_equals |> snd
    1.18 +     |> reveal_bounds Ts)
    1.19    (* A type variable of sort "{}" will make abstraction fail. *)
    1.20    handle THM _ => t |> do_cheaply_conceal_lambdas Ts
    1.21  val introduce_combinators = simple_translate_lambdas do_introduce_combinators
    1.22 @@ -1255,7 +1253,7 @@
    1.23    in
    1.24      t |> need_trueprop ? HOLogic.mk_Trueprop
    1.25        |> (if is_ho then unextensionalize_def
    1.26 -          else cong_extensionalize_term thy #> abs_extensionalize_term ctxt)
    1.27 +          else cong_extensionalize_term ctxt #> abs_extensionalize_term ctxt)
    1.28        |> presimplify_term ctxt
    1.29        |> HOLogic.dest_Trueprop
    1.30    end
     2.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Fri Mar 06 23:44:51 2015 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Fri Mar 06 23:44:57 2015 +0100
     2.3 @@ -41,7 +41,7 @@
     2.4    val hol_open_form : (string -> string) -> term -> term
     2.5    val monomorphic_term : Type.tyenv -> term -> term
     2.6    val eta_expand : typ list -> term -> int -> term
     2.7 -  val cong_extensionalize_term : theory -> term -> term
     2.8 +  val cong_extensionalize_term : Proof.context -> term -> term
     2.9    val abs_extensionalize_term : Proof.context -> term -> term
    2.10    val unextensionalize_def : term -> term
    2.11    val transform_elim_prop : term -> term
    2.12 @@ -338,10 +338,10 @@
    2.13               (List.take (binder_types (fastype_of1 (Ts, t)), n))
    2.14               (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
    2.15  
    2.16 -fun cong_extensionalize_term thy t =
    2.17 +fun cong_extensionalize_term ctxt t =
    2.18    if exists_Const (fn (s, _) => s = @{const_name Not}) t then
    2.19 -    t |> Skip_Proof.make_thm thy
    2.20 -      |> Meson.cong_extensionalize_thm thy
    2.21 +    t |> Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
    2.22 +      |> Meson.cong_extensionalize_thm ctxt
    2.23        |> Thm.prop_of
    2.24    else
    2.25      t
    2.26 @@ -352,10 +352,8 @@
    2.27  
    2.28  fun abs_extensionalize_term ctxt t =
    2.29    if exists_Const is_fun_equality t then
    2.30 -    let val thy = Proof_Context.theory_of ctxt in
    2.31 -      t |> Thm.global_cterm_of thy |> Meson.abs_extensionalize_conv ctxt
    2.32 -        |> Thm.prop_of |> Logic.dest_equals |> snd
    2.33 -    end
    2.34 +    t |> Thm.cterm_of ctxt |> Meson.abs_extensionalize_conv ctxt
    2.35 +      |> Thm.prop_of |> Logic.dest_equals |> snd
    2.36    else
    2.37      t
    2.38  
     3.1 --- a/src/HOL/Tools/Meson/meson.ML	Fri Mar 06 23:44:51 2015 +0100
     3.2 +++ b/src/HOL/Tools/Meson/meson.ML	Fri Mar 06 23:44:57 2015 +0100
     3.3 @@ -22,7 +22,7 @@
     3.4    val choice_theorems : theory -> thm list
     3.5    val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
     3.6    val skolemize : Proof.context -> thm -> thm
     3.7 -  val cong_extensionalize_thm : theory -> thm -> thm
     3.8 +  val cong_extensionalize_thm : Proof.context -> thm -> thm
     3.9    val abs_extensionalize_conv : Proof.context -> conv
    3.10    val abs_extensionalize_thm : Proof.context -> thm -> thm
    3.11    val make_clauses_unsorted: Proof.context -> thm list -> thm list
    3.12 @@ -174,7 +174,7 @@
    3.13    case (Thm.concl_of st, Thm.prop_of th) of
    3.14      (@{const Trueprop} $ (Var _ $ (c as Free _)), @{const Trueprop} $ _) =>
    3.15      let
    3.16 -      val cc = Thm.global_cterm_of (Thm.theory_of_thm th) c
    3.17 +      val cc = Thm.cterm_of ctxt c
    3.18        val ct = Thm.dest_arg (Thm.cprop_of th)
    3.19      in resolve_tac ctxt [th] i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
    3.20    | _ => resolve_tac ctxt [th] i st
    3.21 @@ -622,14 +622,14 @@
    3.22    |> the_single |> Var
    3.23  
    3.24  (* Strengthens "f g ~= f h" to "f g ~= f h & (EX x. g x ~= h x)". *)
    3.25 -fun cong_extensionalize_thm thy th =
    3.26 +fun cong_extensionalize_thm ctxt th =
    3.27    (case Thm.concl_of th of
    3.28      @{const Trueprop} $ (@{const Not}
    3.29          $ (Const (@{const_name HOL.eq}, Type (_, [T, _]))
    3.30             $ (t as _ $ _) $ (u as _ $ _))) =>
    3.31      (case get_F_pattern T t u of
    3.32         SOME p =>
    3.33 -       let val inst = [apply2 (Thm.global_cterm_of thy) (F_ext_cong_neq, p)] in
    3.34 +       let val inst = [apply2 (Thm.cterm_of ctxt) (F_ext_cong_neq, p)] in
    3.35           th RS cterm_instantiate inst ext_cong_neq
    3.36         end
    3.37       | NONE => th)
    3.38 @@ -651,8 +651,7 @@
    3.39  
    3.40  fun try_skolemize_etc ctxt th =
    3.41    let
    3.42 -    val thy = Proof_Context.theory_of ctxt
    3.43 -    val th = th |> cong_extensionalize_thm thy
    3.44 +    val th = th |> cong_extensionalize_thm ctxt
    3.45    in
    3.46      [th]
    3.47      (* Extensionalize lambdas in "th", because that makes sense and that's what
     4.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Mar 06 23:44:51 2015 +0100
     4.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Fri Mar 06 23:44:57 2015 +0100
     4.3 @@ -35,8 +35,8 @@
     4.4  
     4.5  (**** Transformation of Elimination Rules into First-Order Formulas****)
     4.6  
     4.7 -val cfalse = Thm.global_cterm_of @{theory HOL} @{term False};
     4.8 -val ctp_false = Thm.global_cterm_of @{theory HOL} (HOLogic.mk_Trueprop @{term False});
     4.9 +val cfalse = Thm.cterm_of @{theory_context HOL} @{term False};
    4.10 +val ctp_false = Thm.cterm_of @{theory_context HOL} (HOLogic.mk_Trueprop @{term False});
    4.11  
    4.12  (* Converts an elim-rule into an equivalent theorem that does not have the
    4.13     predicate variable. Leaves other theorems unchanged. We simply instantiate
    4.14 @@ -45,9 +45,9 @@
    4.15  fun transform_elim_theorem th =
    4.16    (case Thm.concl_of th of    (*conclusion variable*)
    4.17      @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
    4.18 -      Thm.instantiate ([], [(Thm.global_cterm_of @{theory HOL} v, cfalse)]) th
    4.19 +      Thm.instantiate ([], [(Thm.cterm_of @{theory_context HOL} v, cfalse)]) th
    4.20    | v as Var(_, @{typ prop}) =>
    4.21 -      Thm.instantiate ([], [(Thm.global_cterm_of @{theory HOL} v, ctp_false)]) th
    4.22 +      Thm.instantiate ([], [(Thm.cterm_of @{theory_context HOL} v, ctp_false)]) th
    4.23    | _ => th)
    4.24  
    4.25  
    4.26 @@ -94,9 +94,9 @@
    4.27    | is_quasi_lambda_free (Abs _) = false
    4.28    | is_quasi_lambda_free _ = true
    4.29  
    4.30 -val [f_B,g_B] = map (Thm.global_cterm_of @{theory}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_B}));
    4.31 -val [g_C,f_C] = map (Thm.global_cterm_of @{theory}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_C}));
    4.32 -val [f_S,g_S] = map (Thm.global_cterm_of @{theory}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_S}));
    4.33 +val [f_B,g_B] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_B}));
    4.34 +val [g_C,f_C] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_C}));
    4.35 +val [f_S,g_S] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_S}));
    4.36  
    4.37  (* FIXME: Requires more use of cterm constructors. *)
    4.38  fun abstract ct =
    4.39 @@ -179,7 +179,7 @@
    4.40              TrueI)
    4.41  
    4.42  (*cterms are used throughout for efficiency*)
    4.43 -val cTrueprop = Thm.global_cterm_of @{theory HOL} HOLogic.Trueprop;
    4.44 +val cTrueprop = Thm.cterm_of @{theory_context HOL} HOLogic.Trueprop;
    4.45  
    4.46  (*Given an abstraction over n variables, replace the bound variables by free
    4.47    ones. Return the body, along with the list of free variables.*)
    4.48 @@ -193,8 +193,7 @@
    4.49     Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
    4.50  fun old_skolem_theorem_of_def ctxt rhs0 =
    4.51    let
    4.52 -    val thy = Proof_Context.theory_of ctxt
    4.53 -    val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.global_cterm_of thy
    4.54 +    val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of ctxt
    4.55      val rhs' = rhs |> Thm.dest_comb |> snd
    4.56      val (ch, frees) = c_variant_abs_multi (rhs', [])
    4.57      val (hilbert, cabs) = ch |> Thm.dest_comb |>> Thm.term_of
    4.58 @@ -202,15 +201,16 @@
    4.59        case hilbert of
    4.60          Const (_, Type (@{type_name fun}, [_, T])) => T
    4.61        | _ => raise TERM ("old_skolem_theorem_of_def: expected \"Eps\"", [hilbert])
    4.62 -    val cex = Thm.global_cterm_of thy (HOLogic.exists_const T)
    4.63 +    val cex = Thm.cterm_of ctxt (HOLogic.exists_const T)
    4.64      val ex_tm = Thm.apply cTrueprop (Thm.apply cex cabs)
    4.65      val conc =
    4.66        Drule.list_comb (rhs, frees)
    4.67        |> Drule.beta_conv cabs |> Thm.apply cTrueprop
    4.68      fun tacf [prem] =
    4.69        rewrite_goals_tac ctxt @{thms skolem_def [abs_def]}
    4.70 -      THEN resolve_tac ctxt [(prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]})
    4.71 -                 RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex"] 1
    4.72 +      THEN resolve_tac ctxt
    4.73 +        [(prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]})
    4.74 +          RS Global_Theory.get_thm (Proof_Context.theory_of ctxt) "Hilbert_Choice.someI_ex"] 1
    4.75    in
    4.76      Goal.prove_internal ctxt [ex_tm] conc tacf
    4.77      |> forall_intr_list frees
    4.78 @@ -309,7 +309,7 @@
    4.79           |> new_skolem ? forall_intr_vars
    4.80      val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
    4.81      val th = th |> Conv.fconv_rule (Object_Logic.atomize ctxt)
    4.82 -                |> cong_extensionalize_thm thy
    4.83 +                |> cong_extensionalize_thm ctxt
    4.84                  |> abs_extensionalize_thm ctxt
    4.85                  |> make_nnf ctxt
    4.86    in
    4.87 @@ -334,7 +334,7 @@
    4.88            |> (if no_choice then
    4.89                  Skip_Proof.make_thm thy #> skolemize [cheat_choice] #> Thm.cprop_of
    4.90                else
    4.91 -                Thm.global_cterm_of thy)
    4.92 +                Thm.cterm_of ctxt)
    4.93            |> zap true
    4.94          val fixes =
    4.95            [] |> Term.add_free_names (Thm.prop_of zapped_th)
    4.96 @@ -350,7 +350,7 @@
    4.97            let
    4.98              val (fully_skolemized_ct, ctxt) =
    4.99                Variable.import_terms true [fully_skolemized_t] ctxt
   4.100 -              |>> the_single |>> Thm.global_cterm_of thy
   4.101 +              |>> the_single |>> Thm.cterm_of ctxt
   4.102            in
   4.103              (SOME (discharger_th, fully_skolemized_ct),
   4.104               (Thm.assume fully_skolemized_ct, ctxt))
   4.105 @@ -377,7 +377,7 @@
   4.106         th ctxt
   4.107      val (cnf_ths, ctxt) = clausify nnf_th
   4.108      fun intr_imp ct th =
   4.109 -      Thm.instantiate ([], map (apply2 (Thm.global_cterm_of thy))
   4.110 +      Thm.instantiate ([], map (apply2 (Thm.cterm_of ctxt))
   4.111                                 [(Var (("i", 0), @{typ nat}),
   4.112                                   HOLogic.mk_nat ax_no)])
   4.113                        (zero_var_indexes @{thm skolem_COMBK_D})
     5.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Mar 06 23:44:51 2015 +0100
     5.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Mar 06 23:44:57 2015 +0100
     5.3 @@ -88,7 +88,8 @@
     5.4    the (AList.lookup (uncurry Metis_Thm.equal) th_pairs fth)
     5.5    handle Option.Option => raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
     5.6  
     5.7 -fun cterm_incr_types thy idx = Thm.global_cterm_of thy o map_types (Logic.incr_tvar idx)
     5.8 +fun cterm_incr_types ctxt idx =
     5.9 +  Thm.cterm_of ctxt o map_types (Logic.incr_tvar idx)
    5.10  
    5.11  (* INFERENCE RULE: AXIOM *)
    5.12  
    5.13 @@ -100,17 +101,17 @@
    5.14  
    5.15  val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
    5.16  
    5.17 -fun inst_excluded_middle thy i_atom =
    5.18 +fun inst_excluded_middle ctxt i_atom =
    5.19    let
    5.20      val th = EXCLUDED_MIDDLE
    5.21      val [vx] = Term.add_vars (Thm.prop_of th) []
    5.22 -    val substs = [(Thm.global_cterm_of thy (Var vx), Thm.global_cterm_of thy i_atom)]
    5.23 +    val substs = [(Thm.cterm_of ctxt (Var vx), Thm.cterm_of ctxt i_atom)]
    5.24    in
    5.25      cterm_instantiate substs th
    5.26    end
    5.27  
    5.28  fun assume_inference ctxt type_enc concealed sym_tab atom =
    5.29 -  inst_excluded_middle (Proof_Context.theory_of ctxt)
    5.30 +  inst_excluded_middle ctxt
    5.31      (singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom))
    5.32  
    5.33  (* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
    5.34 @@ -120,7 +121,6 @@
    5.35  
    5.36  fun inst_inference ctxt type_enc concealed sym_tab th_pairs fsubst th =
    5.37    let
    5.38 -    val thy = Proof_Context.theory_of ctxt
    5.39      val i_th = lookth th_pairs th
    5.40      val i_th_vars = Term.add_vars (Thm.prop_of i_th) []
    5.41  
    5.42 @@ -131,7 +131,7 @@
    5.43          (* We call "polish_hol_terms" below. *)
    5.44          val t = hol_term_of_metis ctxt type_enc sym_tab y
    5.45        in
    5.46 -        SOME (Thm.global_cterm_of thy (Var v), t)
    5.47 +        SOME (Thm.cterm_of ctxt (Var v), t)
    5.48        end
    5.49        handle Option.Option =>
    5.50               (trace_msg ctxt (fn () =>
    5.51 @@ -155,7 +155,7 @@
    5.52      val (vars, tms) =
    5.53        ListPair.unzip (map_filter subst_translation substs)
    5.54        ||> polish_hol_terms ctxt concealed
    5.55 -    val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
    5.56 +    val ctm_of = cterm_incr_types ctxt (1 + Thm.maxidx_of i_th)
    5.57      val substs' = ListPair.zip (vars, map ctm_of tms)
    5.58      val _ = trace_msg ctxt (fn () =>
    5.59        cat_lines ("subst_translations:" ::
    5.60 @@ -205,7 +205,6 @@
    5.61      res (tha, thb)
    5.62      handle TERM z =>
    5.63        let
    5.64 -        val thy = Proof_Context.theory_of ctxt
    5.65          val ps = []
    5.66            |> fold (Term.add_vars o Thm.prop_of) [tha, thb]
    5.67            |> AList.group (op =)
    5.68 @@ -213,7 +212,7 @@
    5.69            |> rpair (Envir.empty ~1)
    5.70            |-> fold (Pattern.unify (Context.Proof ctxt))
    5.71            |> Envir.type_env |> Vartab.dest
    5.72 -          |> map (fn (x, (S, T)) => apply2 (Thm.global_ctyp_of thy) (TVar (x, S), T))
    5.73 +          |> map (fn (x, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (x, S), T))
    5.74        in
    5.75          (* The unifier, which is invoked from "Thm.bicompose", will sometimes refuse to unify
    5.76             "?a::?'a" with "?a::?'b" or "?a::nat" and throw a "TERM" exception (with "add_ffpair" as
    5.77 @@ -303,15 +302,14 @@
    5.78  
    5.79  val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
    5.80  
    5.81 -val refl_x = Thm.global_cterm_of @{theory} (Var (hd (Term.add_vars (Thm.prop_of REFL_THM) [])));
    5.82 +val refl_x = Thm.cterm_of @{context} (Var (hd (Term.add_vars (Thm.prop_of REFL_THM) [])));
    5.83  val refl_idx = 1 + Thm.maxidx_of REFL_THM;
    5.84  
    5.85  fun refl_inference ctxt type_enc concealed sym_tab t =
    5.86    let
    5.87 -    val thy = Proof_Context.theory_of ctxt
    5.88      val i_t = singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) t
    5.89      val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
    5.90 -    val c_t = cterm_incr_types thy refl_idx i_t
    5.91 +    val c_t = cterm_incr_types ctxt refl_idx i_t
    5.92    in cterm_instantiate [(refl_x, c_t)] REFL_THM end
    5.93  
    5.94  (* INFERENCE RULE: EQUALITY *)
    5.95 @@ -374,8 +372,9 @@
    5.96        val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill-typed but gives right max*)
    5.97        val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
    5.98        val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
    5.99 -      val eq_terms = map (apply2 (Thm.global_cterm_of thy))
   5.100 -        (ListPair.zip (Misc_Legacy.term_vars (Thm.prop_of subst'), [tm_abs, tm_subst, i_tm]))
   5.101 +      val eq_terms =
   5.102 +        map (apply2 (Thm.cterm_of ctxt))
   5.103 +          (ListPair.zip (Misc_Legacy.term_vars (Thm.prop_of subst'), [tm_abs, tm_subst, i_tm]))
   5.104    in
   5.105      cterm_instantiate eq_terms subst'
   5.106    end
   5.107 @@ -477,7 +476,7 @@
   5.108     variables before applying "assume_tac". Typical constraints are of the form
   5.109       ?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x,
   5.110     where the nonvariables are goal parameters. *)
   5.111 -fun unify_first_prem_with_concl thy i th =
   5.112 +fun unify_first_prem_with_concl ctxt i th =
   5.113    let
   5.114      val goal = Logic.get_goal (Thm.prop_of th) i |> Envir.beta_eta_contract
   5.115      val prem = goal |> Logic.strip_assums_hyp |> hd
   5.116 @@ -520,7 +519,7 @@
   5.117        | _ => I)
   5.118  
   5.119      val t_inst =
   5.120 -      [] |> try (unify_terms (prem, concl) #> map (apply2 (Thm.global_cterm_of thy)))
   5.121 +      [] |> try (unify_terms (prem, concl) #> map (apply2 (Thm.cterm_of ctxt)))
   5.122           |> the_default [] (* FIXME *)
   5.123    in
   5.124      cterm_instantiate t_inst th
   5.125 @@ -539,8 +538,6 @@
   5.126  
   5.127  fun instantiate_forall_tac ctxt t i st =
   5.128    let
   5.129 -    val thy = Proof_Context.theory_of ctxt
   5.130 -
   5.131      val params = Logic.strip_params (Logic.get_goal (Thm.prop_of st) i) |> rev
   5.132  
   5.133      fun repair (t as (Var ((s, _), _))) =
   5.134 @@ -574,9 +571,9 @@
   5.135              Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0,
   5.136                tenv = Vartab.empty, tyenv = tyenv}
   5.137            val ty_inst =
   5.138 -            Vartab.fold (fn (x, (S, T)) => cons (apply2 (Thm.global_ctyp_of thy) (TVar (x, S), T)))
   5.139 +            Vartab.fold (fn (x, (S, T)) => cons (apply2 (Thm.ctyp_of ctxt) (TVar (x, S), T)))
   5.140                tyenv []
   5.141 -          val t_inst = [apply2 (Thm.global_cterm_of thy o Envir.norm_term env) (Var var, t')]
   5.142 +          val t_inst = [apply2 (Thm.cterm_of ctxt o Envir.norm_term env) (Var var, t')]
   5.143          in
   5.144            Drule.instantiate_normalize (ty_inst, t_inst) th
   5.145          end
   5.146 @@ -747,7 +744,7 @@
   5.147              THEN match_tac ctxt' [prems_imp_false] 1
   5.148              THEN ALLGOALS (fn i => resolve_tac ctxt' @{thms Meson.skolem_COMBK_I} i
   5.149                THEN rotate_tac (rotation_of_subgoal i) i
   5.150 -              THEN PRIMITIVE (unify_first_prem_with_concl thy i)
   5.151 +              THEN PRIMITIVE (unify_first_prem_with_concl ctxt' i)
   5.152                THEN assume_tac ctxt' i
   5.153                THEN flexflex_tac ctxt')))
   5.154        handle ERROR msg =>
     6.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Fri Mar 06 23:44:51 2015 +0100
     6.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Fri Mar 06 23:44:57 2015 +0100
     6.3 @@ -44,26 +44,23 @@
     6.4     In Isabelle, type tags are stripped away, so we are left with "t = t" or
     6.5     "t => t". Type tag idempotence is also handled this way. *)
     6.6  fun reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth =
     6.7 -  let val thy = Proof_Context.theory_of ctxt in
     6.8 -    (case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of
     6.9 -      Const (@{const_name HOL.eq}, _) $ _ $ t =>
    6.10 -      let
    6.11 -        val ct = Thm.global_cterm_of thy t
    6.12 -        val cT = Thm.ctyp_of_cterm ct
    6.13 -      in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
    6.14 -    | Const (@{const_name disj}, _) $ t1 $ t2 =>
    6.15 -      (if can HOLogic.dest_not t1 then t2 else t1)
    6.16 -      |> HOLogic.mk_Trueprop |> Thm.global_cterm_of thy |> Thm.trivial
    6.17 -    | _ => raise Fail "expected reflexive or trivial clause")
    6.18 -  end
    6.19 +  (case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of
    6.20 +    Const (@{const_name HOL.eq}, _) $ _ $ t =>
    6.21 +    let
    6.22 +      val ct = Thm.cterm_of ctxt t
    6.23 +      val cT = Thm.ctyp_of_cterm ct
    6.24 +    in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
    6.25 +  | Const (@{const_name disj}, _) $ t1 $ t2 =>
    6.26 +    (if can HOLogic.dest_not t1 then t2 else t1)
    6.27 +    |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial
    6.28 +  | _ => raise Fail "expected reflexive or trivial clause")
    6.29    |> Meson.make_meta_clause
    6.30  
    6.31  fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth =
    6.32    let
    6.33 -    val thy = Proof_Context.theory_of ctxt
    6.34      val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN resolve_tac ctxt [refl] 1
    6.35      val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth
    6.36 -    val ct = Thm.global_cterm_of thy (HOLogic.mk_Trueprop t)
    6.37 +    val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t)
    6.38    in Goal.prove_internal ctxt [] ct (K tac) |> Meson.make_meta_clause end
    6.39  
    6.40  fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u]
    6.41 @@ -77,7 +74,6 @@
    6.42      th
    6.43    else
    6.44      let
    6.45 -      val thy = Proof_Context.theory_of ctxt
    6.46        fun conv first ctxt ct =
    6.47          if Meson_Clausify.is_quasi_lambda_free (Thm.term_of ct) then
    6.48            Thm.reflexive ct
    6.49 @@ -91,7 +87,7 @@
    6.50                  |> (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI})
    6.51                | v :: _ =>
    6.52                  Abs (Name.uu, fastype_of v, abstract_over (v, Thm.term_of ct)) $ v
    6.53 -                |> Thm.global_cterm_of thy
    6.54 +                |> Thm.cterm_of ctxt
    6.55                  |> Conv.comb_conv (conv true ctxt))
    6.56              else
    6.57                Conv.abs_conv (conv false o snd) ctxt ct
    6.58 @@ -101,7 +97,7 @@
    6.59        (* We replace the equation's left-hand side with a beta-equivalent term
    6.60           so that "Thm.equal_elim" works below. *)
    6.61        val t0 $ _ $ t2 = Thm.prop_of eq_th
    6.62 -      val eq_ct = t0 $ Thm.prop_of th $ t2 |> Thm.global_cterm_of thy
    6.63 +      val eq_ct = t0 $ Thm.prop_of th $ t2 |> Thm.cterm_of ctxt
    6.64        val eq_th' = Goal.prove_internal ctxt [] eq_ct (K (resolve_tac ctxt [eq_th] 1))
    6.65      in Thm.equal_elim eq_th' th end
    6.66  
     7.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Mar 06 23:44:51 2015 +0100
     7.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Mar 06 23:44:57 2015 +0100
     7.3 @@ -31,7 +31,7 @@
     7.4  (** instantiate elimination rules **)
     7.5  
     7.6  local
     7.7 -  val (cpfalse, cfalse) = `SMT_Util.mk_cprop (Thm.global_cterm_of @{theory} @{const False})
     7.8 +  val (cpfalse, cfalse) = `SMT_Util.mk_cprop (Thm.cterm_of @{context} @{const False})
     7.9  
    7.10    fun inst f ct thm =
    7.11      let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
    7.12 @@ -189,7 +189,7 @@
    7.13    fun mk_pat ct = Thm.apply (SMT_Util.instT' ct pat) ct
    7.14  
    7.15    fun mk_clist T =
    7.16 -    apply2 (Thm.global_cterm_of @{theory}) (SMT_Util.symb_cons_const T, SMT_Util.symb_nil_const T)
    7.17 +    apply2 (Thm.cterm_of @{context}) (SMT_Util.symb_cons_const T, SMT_Util.symb_nil_const T)
    7.18    fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil
    7.19    val mk_pat_list = mk_list (mk_clist @{typ pattern})
    7.20    val mk_mpat_list = mk_list (mk_clist @{typ "pattern symb_list"})
     8.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Fri Mar 06 23:44:51 2015 +0100
     8.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Fri Mar 06 23:44:57 2015 +0100
     8.3 @@ -64,14 +64,14 @@
     8.4    fun mk_nary _ cu [] = cu
     8.5      | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
     8.6  
     8.7 -  val mk_uminus = Thm.apply (Thm.global_cterm_of @{theory} @{const uminus (real)})
     8.8 -  val add = Thm.global_cterm_of @{theory} @{const plus (real)}
     8.9 +  val mk_uminus = Thm.apply (Thm.cterm_of @{context} @{const uminus (real)})
    8.10 +  val add = Thm.cterm_of @{context} @{const plus (real)}
    8.11    val real0 = Numeral.mk_cnumber @{ctyp real} 0
    8.12 -  val mk_sub = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const minus (real)})
    8.13 -  val mk_mul = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const times (real)})
    8.14 -  val mk_div = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const divide (real)})
    8.15 -  val mk_lt = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less (real)})
    8.16 -  val mk_le = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less_eq (real)})
    8.17 +  val mk_sub = Thm.mk_binop (Thm.cterm_of @{context} @{const minus (real)})
    8.18 +  val mk_mul = Thm.mk_binop (Thm.cterm_of @{context} @{const times (real)})
    8.19 +  val mk_div = Thm.mk_binop (Thm.cterm_of @{context} @{const divide (real)})
    8.20 +  val mk_lt = Thm.mk_binop (Thm.cterm_of @{context} @{const less (real)})
    8.21 +  val mk_le = Thm.mk_binop (Thm.cterm_of @{context} @{const less_eq (real)})
    8.22  
    8.23    fun z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
    8.24      | z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) cts = SOME (mk_nary add real0 cts)
     9.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Mar 06 23:44:51 2015 +0100
     9.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Mar 06 23:44:57 2015 +0100
     9.3 @@ -207,7 +207,7 @@
     9.4          else oracle ()
     9.5      | (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat)))
     9.6  
     9.7 -  val cfalse = Thm.global_cterm_of @{theory} @{prop False}
     9.8 +  val cfalse = Thm.cterm_of @{context} @{prop False}
     9.9  in
    9.10  
    9.11  fun add_solver ({name, class, avail, command, options, smt_options, default_max_relevant, outcome,
    10.1 --- a/src/HOL/Tools/SMT/smt_util.ML	Fri Mar 06 23:44:51 2015 +0100
    10.2 +++ b/src/HOL/Tools/SMT/smt_util.ML	Fri Mar 06 23:44:57 2015 +0100
    10.3 @@ -194,7 +194,7 @@
    10.4  
    10.5  val dest_all_cbinders = repeat_yield (try o dest_cbinder)
    10.6  
    10.7 -val mk_cprop = Thm.apply (Thm.global_cterm_of @{theory} @{const Trueprop})
    10.8 +val mk_cprop = Thm.apply (Thm.cterm_of @{context} @{const Trueprop})
    10.9  
   10.10  fun dest_cprop ct =
   10.11    (case Thm.term_of ct of
    11.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Fri Mar 06 23:44:51 2015 +0100
    11.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Fri Mar 06 23:44:57 2015 +0100
    11.3 @@ -112,13 +112,13 @@
    11.4    | mk_builtin_num ctxt i T =
    11.5        chained_mk_builtin_num ctxt (get_mk_builtins ctxt) i T
    11.6  
    11.7 -val mk_true = Thm.global_cterm_of @{theory} (@{const Not} $ @{const False})
    11.8 -val mk_false = Thm.global_cterm_of @{theory} @{const False}
    11.9 -val mk_not = Thm.apply (Thm.global_cterm_of @{theory} @{const Not})
   11.10 -val mk_implies = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const HOL.implies})
   11.11 -val mk_iff = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const HOL.eq (bool)})
   11.12 -val conj = Thm.global_cterm_of @{theory} @{const HOL.conj}
   11.13 -val disj = Thm.global_cterm_of @{theory} @{const HOL.disj}
   11.14 +val mk_true = Thm.cterm_of @{context} (@{const Not} $ @{const False})
   11.15 +val mk_false = Thm.cterm_of @{context} @{const False}
   11.16 +val mk_not = Thm.apply (Thm.cterm_of @{context} @{const Not})
   11.17 +val mk_implies = Thm.mk_binop (Thm.cterm_of @{context} @{const HOL.implies})
   11.18 +val mk_iff = Thm.mk_binop (Thm.cterm_of @{context} @{const HOL.eq (bool)})
   11.19 +val conj = Thm.cterm_of @{context} @{const HOL.conj}
   11.20 +val disj = Thm.cterm_of @{context} @{const HOL.disj}
   11.21  
   11.22  fun mk_nary _ cu [] = cu
   11.23    | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
   11.24 @@ -139,15 +139,15 @@
   11.25    let val cTs = Thm.dest_ctyp (Thm.ctyp_of_cterm array)
   11.26    in Thm.apply (Thm.mk_binop (SMT_Util.instTs cTs update) array index) value end
   11.27  
   11.28 -val mk_uminus = Thm.apply (Thm.global_cterm_of @{theory} @{const uminus (int)})
   11.29 -val add = Thm.global_cterm_of @{theory} @{const plus (int)}
   11.30 +val mk_uminus = Thm.apply (Thm.cterm_of @{context} @{const uminus (int)})
   11.31 +val add = Thm.cterm_of @{context} @{const plus (int)}
   11.32  val int0 = Numeral.mk_cnumber @{ctyp int} 0
   11.33 -val mk_sub = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const minus (int)})
   11.34 -val mk_mul = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const times (int)})
   11.35 -val mk_div = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const z3div})
   11.36 -val mk_mod = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const z3mod})
   11.37 -val mk_lt = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less (int)})
   11.38 -val mk_le = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less_eq (int)})
   11.39 +val mk_sub = Thm.mk_binop (Thm.cterm_of @{context} @{const minus (int)})
   11.40 +val mk_mul = Thm.mk_binop (Thm.cterm_of @{context} @{const times (int)})
   11.41 +val mk_div = Thm.mk_binop (Thm.cterm_of @{context} @{const z3div})
   11.42 +val mk_mod = Thm.mk_binop (Thm.cterm_of @{context} @{const z3mod})
   11.43 +val mk_lt = Thm.mk_binop (Thm.cterm_of @{context} @{const less (int)})
   11.44 +val mk_le = Thm.mk_binop (Thm.cterm_of @{context} @{const less_eq (int)})
   11.45  
   11.46  fun mk_builtin_fun ctxt sym cts =
   11.47    (case (sym, cts) of