--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Mar 06 23:44:51 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Mar 06 23:44:57 2015 +0100
@@ -758,13 +758,11 @@
(0 upto length Ts - 1 ~~ Ts))
fun do_introduce_combinators ctxt Ts t =
- let val thy = Proof_Context.theory_of ctxt in
- t |> conceal_bounds Ts
- |> Thm.global_cterm_of thy
- |> Meson_Clausify.introduce_combinators_in_cterm
- |> Thm.prop_of |> Logic.dest_equals |> snd
- |> reveal_bounds Ts
- end
+ (t |> conceal_bounds Ts
+ |> Thm.cterm_of ctxt
+ |> Meson_Clausify.introduce_combinators_in_cterm
+ |> Thm.prop_of |> Logic.dest_equals |> snd
+ |> reveal_bounds Ts)
(* A type variable of sort "{}" will make abstraction fail. *)
handle THM _ => t |> do_cheaply_conceal_lambdas Ts
val introduce_combinators = simple_translate_lambdas do_introduce_combinators
@@ -1255,7 +1253,7 @@
in
t |> need_trueprop ? HOLogic.mk_Trueprop
|> (if is_ho then unextensionalize_def
- else cong_extensionalize_term thy #> abs_extensionalize_term ctxt)
+ else cong_extensionalize_term ctxt #> abs_extensionalize_term ctxt)
|> presimplify_term ctxt
|> HOLogic.dest_Trueprop
end
--- a/src/HOL/Tools/ATP/atp_util.ML Fri Mar 06 23:44:51 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML Fri Mar 06 23:44:57 2015 +0100
@@ -41,7 +41,7 @@
val hol_open_form : (string -> string) -> term -> term
val monomorphic_term : Type.tyenv -> term -> term
val eta_expand : typ list -> term -> int -> term
- val cong_extensionalize_term : theory -> term -> term
+ val cong_extensionalize_term : Proof.context -> term -> term
val abs_extensionalize_term : Proof.context -> term -> term
val unextensionalize_def : term -> term
val transform_elim_prop : term -> term
@@ -338,10 +338,10 @@
(List.take (binder_types (fastype_of1 (Ts, t)), n))
(list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
-fun cong_extensionalize_term thy t =
+fun cong_extensionalize_term ctxt t =
if exists_Const (fn (s, _) => s = @{const_name Not}) t then
- t |> Skip_Proof.make_thm thy
- |> Meson.cong_extensionalize_thm thy
+ t |> Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
+ |> Meson.cong_extensionalize_thm ctxt
|> Thm.prop_of
else
t
@@ -352,10 +352,8 @@
fun abs_extensionalize_term ctxt t =
if exists_Const is_fun_equality t then
- let val thy = Proof_Context.theory_of ctxt in
- t |> Thm.global_cterm_of thy |> Meson.abs_extensionalize_conv ctxt
- |> Thm.prop_of |> Logic.dest_equals |> snd
- end
+ t |> Thm.cterm_of ctxt |> Meson.abs_extensionalize_conv ctxt
+ |> Thm.prop_of |> Logic.dest_equals |> snd
else
t
--- a/src/HOL/Tools/Meson/meson.ML Fri Mar 06 23:44:51 2015 +0100
+++ b/src/HOL/Tools/Meson/meson.ML Fri Mar 06 23:44:57 2015 +0100
@@ -22,7 +22,7 @@
val choice_theorems : theory -> thm list
val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
val skolemize : Proof.context -> thm -> thm
- val cong_extensionalize_thm : theory -> thm -> thm
+ val cong_extensionalize_thm : Proof.context -> thm -> thm
val abs_extensionalize_conv : Proof.context -> conv
val abs_extensionalize_thm : Proof.context -> thm -> thm
val make_clauses_unsorted: Proof.context -> thm list -> thm list
@@ -174,7 +174,7 @@
case (Thm.concl_of st, Thm.prop_of th) of
(@{const Trueprop} $ (Var _ $ (c as Free _)), @{const Trueprop} $ _) =>
let
- val cc = Thm.global_cterm_of (Thm.theory_of_thm th) c
+ val cc = Thm.cterm_of ctxt c
val ct = Thm.dest_arg (Thm.cprop_of th)
in resolve_tac ctxt [th] i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
| _ => resolve_tac ctxt [th] i st
@@ -622,14 +622,14 @@
|> the_single |> Var
(* Strengthens "f g ~= f h" to "f g ~= f h & (EX x. g x ~= h x)". *)
-fun cong_extensionalize_thm thy th =
+fun cong_extensionalize_thm ctxt th =
(case Thm.concl_of th of
@{const Trueprop} $ (@{const Not}
$ (Const (@{const_name HOL.eq}, Type (_, [T, _]))
$ (t as _ $ _) $ (u as _ $ _))) =>
(case get_F_pattern T t u of
SOME p =>
- let val inst = [apply2 (Thm.global_cterm_of thy) (F_ext_cong_neq, p)] in
+ let val inst = [apply2 (Thm.cterm_of ctxt) (F_ext_cong_neq, p)] in
th RS cterm_instantiate inst ext_cong_neq
end
| NONE => th)
@@ -651,8 +651,7 @@
fun try_skolemize_etc ctxt th =
let
- val thy = Proof_Context.theory_of ctxt
- val th = th |> cong_extensionalize_thm thy
+ val th = th |> cong_extensionalize_thm ctxt
in
[th]
(* Extensionalize lambdas in "th", because that makes sense and that's what
--- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Mar 06 23:44:51 2015 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Mar 06 23:44:57 2015 +0100
@@ -35,8 +35,8 @@
(**** Transformation of Elimination Rules into First-Order Formulas****)
-val cfalse = Thm.global_cterm_of @{theory HOL} @{term False};
-val ctp_false = Thm.global_cterm_of @{theory HOL} (HOLogic.mk_Trueprop @{term False});
+val cfalse = Thm.cterm_of @{theory_context HOL} @{term False};
+val ctp_false = Thm.cterm_of @{theory_context HOL} (HOLogic.mk_Trueprop @{term False});
(* Converts an elim-rule into an equivalent theorem that does not have the
predicate variable. Leaves other theorems unchanged. We simply instantiate
@@ -45,9 +45,9 @@
fun transform_elim_theorem th =
(case Thm.concl_of th of (*conclusion variable*)
@{const Trueprop} $ (v as Var (_, @{typ bool})) =>
- Thm.instantiate ([], [(Thm.global_cterm_of @{theory HOL} v, cfalse)]) th
+ Thm.instantiate ([], [(Thm.cterm_of @{theory_context HOL} v, cfalse)]) th
| v as Var(_, @{typ prop}) =>
- Thm.instantiate ([], [(Thm.global_cterm_of @{theory HOL} v, ctp_false)]) th
+ Thm.instantiate ([], [(Thm.cterm_of @{theory_context HOL} v, ctp_false)]) th
| _ => th)
@@ -94,9 +94,9 @@
| is_quasi_lambda_free (Abs _) = false
| is_quasi_lambda_free _ = true
-val [f_B,g_B] = map (Thm.global_cterm_of @{theory}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_B}));
-val [g_C,f_C] = map (Thm.global_cterm_of @{theory}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_C}));
-val [f_S,g_S] = map (Thm.global_cterm_of @{theory}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_S}));
+val [f_B,g_B] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_B}));
+val [g_C,f_C] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_C}));
+val [f_S,g_S] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_S}));
(* FIXME: Requires more use of cterm constructors. *)
fun abstract ct =
@@ -179,7 +179,7 @@
TrueI)
(*cterms are used throughout for efficiency*)
-val cTrueprop = Thm.global_cterm_of @{theory HOL} HOLogic.Trueprop;
+val cTrueprop = Thm.cterm_of @{theory_context HOL} HOLogic.Trueprop;
(*Given an abstraction over n variables, replace the bound variables by free
ones. Return the body, along with the list of free variables.*)
@@ -193,8 +193,7 @@
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
fun old_skolem_theorem_of_def ctxt rhs0 =
let
- val thy = Proof_Context.theory_of ctxt
- val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.global_cterm_of thy
+ val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of ctxt
val rhs' = rhs |> Thm.dest_comb |> snd
val (ch, frees) = c_variant_abs_multi (rhs', [])
val (hilbert, cabs) = ch |> Thm.dest_comb |>> Thm.term_of
@@ -202,15 +201,16 @@
case hilbert of
Const (_, Type (@{type_name fun}, [_, T])) => T
| _ => raise TERM ("old_skolem_theorem_of_def: expected \"Eps\"", [hilbert])
- val cex = Thm.global_cterm_of thy (HOLogic.exists_const T)
+ val cex = Thm.cterm_of ctxt (HOLogic.exists_const T)
val ex_tm = Thm.apply cTrueprop (Thm.apply cex cabs)
val conc =
Drule.list_comb (rhs, frees)
|> Drule.beta_conv cabs |> Thm.apply cTrueprop
fun tacf [prem] =
rewrite_goals_tac ctxt @{thms skolem_def [abs_def]}
- THEN resolve_tac ctxt [(prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]})
- RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex"] 1
+ THEN resolve_tac ctxt
+ [(prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]})
+ RS Global_Theory.get_thm (Proof_Context.theory_of ctxt) "Hilbert_Choice.someI_ex"] 1
in
Goal.prove_internal ctxt [ex_tm] conc tacf
|> forall_intr_list frees
@@ -309,7 +309,7 @@
|> new_skolem ? forall_intr_vars
val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
val th = th |> Conv.fconv_rule (Object_Logic.atomize ctxt)
- |> cong_extensionalize_thm thy
+ |> cong_extensionalize_thm ctxt
|> abs_extensionalize_thm ctxt
|> make_nnf ctxt
in
@@ -334,7 +334,7 @@
|> (if no_choice then
Skip_Proof.make_thm thy #> skolemize [cheat_choice] #> Thm.cprop_of
else
- Thm.global_cterm_of thy)
+ Thm.cterm_of ctxt)
|> zap true
val fixes =
[] |> Term.add_free_names (Thm.prop_of zapped_th)
@@ -350,7 +350,7 @@
let
val (fully_skolemized_ct, ctxt) =
Variable.import_terms true [fully_skolemized_t] ctxt
- |>> the_single |>> Thm.global_cterm_of thy
+ |>> the_single |>> Thm.cterm_of ctxt
in
(SOME (discharger_th, fully_skolemized_ct),
(Thm.assume fully_skolemized_ct, ctxt))
@@ -377,7 +377,7 @@
th ctxt
val (cnf_ths, ctxt) = clausify nnf_th
fun intr_imp ct th =
- Thm.instantiate ([], map (apply2 (Thm.global_cterm_of thy))
+ Thm.instantiate ([], map (apply2 (Thm.cterm_of ctxt))
[(Var (("i", 0), @{typ nat}),
HOLogic.mk_nat ax_no)])
(zero_var_indexes @{thm skolem_COMBK_D})
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Mar 06 23:44:51 2015 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Mar 06 23:44:57 2015 +0100
@@ -88,7 +88,8 @@
the (AList.lookup (uncurry Metis_Thm.equal) th_pairs fth)
handle Option.Option => raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
-fun cterm_incr_types thy idx = Thm.global_cterm_of thy o map_types (Logic.incr_tvar idx)
+fun cterm_incr_types ctxt idx =
+ Thm.cterm_of ctxt o map_types (Logic.incr_tvar idx)
(* INFERENCE RULE: AXIOM *)
@@ -100,17 +101,17 @@
val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
-fun inst_excluded_middle thy i_atom =
+fun inst_excluded_middle ctxt i_atom =
let
val th = EXCLUDED_MIDDLE
val [vx] = Term.add_vars (Thm.prop_of th) []
- val substs = [(Thm.global_cterm_of thy (Var vx), Thm.global_cterm_of thy i_atom)]
+ val substs = [(Thm.cterm_of ctxt (Var vx), Thm.cterm_of ctxt i_atom)]
in
cterm_instantiate substs th
end
fun assume_inference ctxt type_enc concealed sym_tab atom =
- inst_excluded_middle (Proof_Context.theory_of ctxt)
+ inst_excluded_middle ctxt
(singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom))
(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
@@ -120,7 +121,6 @@
fun inst_inference ctxt type_enc concealed sym_tab th_pairs fsubst th =
let
- val thy = Proof_Context.theory_of ctxt
val i_th = lookth th_pairs th
val i_th_vars = Term.add_vars (Thm.prop_of i_th) []
@@ -131,7 +131,7 @@
(* We call "polish_hol_terms" below. *)
val t = hol_term_of_metis ctxt type_enc sym_tab y
in
- SOME (Thm.global_cterm_of thy (Var v), t)
+ SOME (Thm.cterm_of ctxt (Var v), t)
end
handle Option.Option =>
(trace_msg ctxt (fn () =>
@@ -155,7 +155,7 @@
val (vars, tms) =
ListPair.unzip (map_filter subst_translation substs)
||> polish_hol_terms ctxt concealed
- val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
+ val ctm_of = cterm_incr_types ctxt (1 + Thm.maxidx_of i_th)
val substs' = ListPair.zip (vars, map ctm_of tms)
val _ = trace_msg ctxt (fn () =>
cat_lines ("subst_translations:" ::
@@ -205,7 +205,6 @@
res (tha, thb)
handle TERM z =>
let
- val thy = Proof_Context.theory_of ctxt
val ps = []
|> fold (Term.add_vars o Thm.prop_of) [tha, thb]
|> AList.group (op =)
@@ -213,7 +212,7 @@
|> rpair (Envir.empty ~1)
|-> fold (Pattern.unify (Context.Proof ctxt))
|> Envir.type_env |> Vartab.dest
- |> map (fn (x, (S, T)) => apply2 (Thm.global_ctyp_of thy) (TVar (x, S), T))
+ |> map (fn (x, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (x, S), T))
in
(* The unifier, which is invoked from "Thm.bicompose", will sometimes refuse to unify
"?a::?'a" with "?a::?'b" or "?a::nat" and throw a "TERM" exception (with "add_ffpair" as
@@ -303,15 +302,14 @@
val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
-val refl_x = Thm.global_cterm_of @{theory} (Var (hd (Term.add_vars (Thm.prop_of REFL_THM) [])));
+val refl_x = Thm.cterm_of @{context} (Var (hd (Term.add_vars (Thm.prop_of REFL_THM) [])));
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
fun refl_inference ctxt type_enc concealed sym_tab t =
let
- val thy = Proof_Context.theory_of ctxt
val i_t = singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) t
val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
- val c_t = cterm_incr_types thy refl_idx i_t
+ val c_t = cterm_incr_types ctxt refl_idx i_t
in cterm_instantiate [(refl_x, c_t)] REFL_THM end
(* INFERENCE RULE: EQUALITY *)
@@ -374,8 +372,9 @@
val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill-typed but gives right max*)
val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
- val eq_terms = map (apply2 (Thm.global_cterm_of thy))
- (ListPair.zip (Misc_Legacy.term_vars (Thm.prop_of subst'), [tm_abs, tm_subst, i_tm]))
+ val eq_terms =
+ map (apply2 (Thm.cterm_of ctxt))
+ (ListPair.zip (Misc_Legacy.term_vars (Thm.prop_of subst'), [tm_abs, tm_subst, i_tm]))
in
cterm_instantiate eq_terms subst'
end
@@ -477,7 +476,7 @@
variables before applying "assume_tac". Typical constraints are of the form
?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,
where the nonvariables are goal parameters. *)
-fun unify_first_prem_with_concl thy i th =
+fun unify_first_prem_with_concl ctxt i th =
let
val goal = Logic.get_goal (Thm.prop_of th) i |> Envir.beta_eta_contract
val prem = goal |> Logic.strip_assums_hyp |> hd
@@ -520,7 +519,7 @@
| _ => I)
val t_inst =
- [] |> try (unify_terms (prem, concl) #> map (apply2 (Thm.global_cterm_of thy)))
+ [] |> try (unify_terms (prem, concl) #> map (apply2 (Thm.cterm_of ctxt)))
|> the_default [] (* FIXME *)
in
cterm_instantiate t_inst th
@@ -539,8 +538,6 @@
fun instantiate_forall_tac ctxt t i st =
let
- val thy = Proof_Context.theory_of ctxt
-
val params = Logic.strip_params (Logic.get_goal (Thm.prop_of st) i) |> rev
fun repair (t as (Var ((s, _), _))) =
@@ -574,9 +571,9 @@
Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0,
tenv = Vartab.empty, tyenv = tyenv}
val ty_inst =
- Vartab.fold (fn (x, (S, T)) => cons (apply2 (Thm.global_ctyp_of thy) (TVar (x, S), T)))
+ Vartab.fold (fn (x, (S, T)) => cons (apply2 (Thm.ctyp_of ctxt) (TVar (x, S), T)))
tyenv []
- val t_inst = [apply2 (Thm.global_cterm_of thy o Envir.norm_term env) (Var var, t')]
+ val t_inst = [apply2 (Thm.cterm_of ctxt o Envir.norm_term env) (Var var, t')]
in
Drule.instantiate_normalize (ty_inst, t_inst) th
end
@@ -747,7 +744,7 @@
THEN match_tac ctxt' [prems_imp_false] 1
THEN ALLGOALS (fn i => resolve_tac ctxt' @{thms Meson.skolem_COMBK_I} i
THEN rotate_tac (rotation_of_subgoal i) i
- THEN PRIMITIVE (unify_first_prem_with_concl thy i)
+ THEN PRIMITIVE (unify_first_prem_with_concl ctxt' i)
THEN assume_tac ctxt' i
THEN flexflex_tac ctxt')))
handle ERROR msg =>
--- a/src/HOL/Tools/Metis/metis_tactic.ML Fri Mar 06 23:44:51 2015 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Fri Mar 06 23:44:57 2015 +0100
@@ -44,26 +44,23 @@
In Isabelle, type tags are stripped away, so we are left with "t = t" or
"t => t". Type tag idempotence is also handled this way. *)
fun reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth =
- let val thy = Proof_Context.theory_of ctxt in
- (case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of
- Const (@{const_name HOL.eq}, _) $ _ $ t =>
- let
- val ct = Thm.global_cterm_of thy t
- val cT = Thm.ctyp_of_cterm ct
- in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
- | Const (@{const_name disj}, _) $ t1 $ t2 =>
- (if can HOLogic.dest_not t1 then t2 else t1)
- |> HOLogic.mk_Trueprop |> Thm.global_cterm_of thy |> Thm.trivial
- | _ => raise Fail "expected reflexive or trivial clause")
- end
+ (case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of
+ Const (@{const_name HOL.eq}, _) $ _ $ t =>
+ let
+ val ct = Thm.cterm_of ctxt t
+ val cT = Thm.ctyp_of_cterm ct
+ in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
+ | Const (@{const_name disj}, _) $ t1 $ t2 =>
+ (if can HOLogic.dest_not t1 then t2 else t1)
+ |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial
+ | _ => raise Fail "expected reflexive or trivial clause")
|> Meson.make_meta_clause
fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth =
let
- val thy = Proof_Context.theory_of ctxt
val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN resolve_tac ctxt [refl] 1
val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth
- val ct = Thm.global_cterm_of thy (HOLogic.mk_Trueprop t)
+ val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t)
in Goal.prove_internal ctxt [] ct (K tac) |> Meson.make_meta_clause end
fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u]
@@ -77,7 +74,6 @@
th
else
let
- val thy = Proof_Context.theory_of ctxt
fun conv first ctxt ct =
if Meson_Clausify.is_quasi_lambda_free (Thm.term_of ct) then
Thm.reflexive ct
@@ -91,7 +87,7 @@
|> (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI})
| v :: _ =>
Abs (Name.uu, fastype_of v, abstract_over (v, Thm.term_of ct)) $ v
- |> Thm.global_cterm_of thy
+ |> Thm.cterm_of ctxt
|> Conv.comb_conv (conv true ctxt))
else
Conv.abs_conv (conv false o snd) ctxt ct
@@ -101,7 +97,7 @@
(* We replace the equation's left-hand side with a beta-equivalent term
so that "Thm.equal_elim" works below. *)
val t0 $ _ $ t2 = Thm.prop_of eq_th
- val eq_ct = t0 $ Thm.prop_of th $ t2 |> Thm.global_cterm_of thy
+ val eq_ct = t0 $ Thm.prop_of th $ t2 |> Thm.cterm_of ctxt
val eq_th' = Goal.prove_internal ctxt [] eq_ct (K (resolve_tac ctxt [eq_th] 1))
in Thm.equal_elim eq_th' th end
--- a/src/HOL/Tools/SMT/smt_normalize.ML Fri Mar 06 23:44:51 2015 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Mar 06 23:44:57 2015 +0100
@@ -31,7 +31,7 @@
(** instantiate elimination rules **)
local
- val (cpfalse, cfalse) = `SMT_Util.mk_cprop (Thm.global_cterm_of @{theory} @{const False})
+ val (cpfalse, cfalse) = `SMT_Util.mk_cprop (Thm.cterm_of @{context} @{const False})
fun inst f ct thm =
let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
@@ -189,7 +189,7 @@
fun mk_pat ct = Thm.apply (SMT_Util.instT' ct pat) ct
fun mk_clist T =
- apply2 (Thm.global_cterm_of @{theory}) (SMT_Util.symb_cons_const T, SMT_Util.symb_nil_const T)
+ apply2 (Thm.cterm_of @{context}) (SMT_Util.symb_cons_const T, SMT_Util.symb_nil_const T)
fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil
val mk_pat_list = mk_list (mk_clist @{typ pattern})
val mk_mpat_list = mk_list (mk_clist @{typ "pattern symb_list"})
--- a/src/HOL/Tools/SMT/smt_real.ML Fri Mar 06 23:44:51 2015 +0100
+++ b/src/HOL/Tools/SMT/smt_real.ML Fri Mar 06 23:44:57 2015 +0100
@@ -64,14 +64,14 @@
fun mk_nary _ cu [] = cu
| mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
- val mk_uminus = Thm.apply (Thm.global_cterm_of @{theory} @{const uminus (real)})
- val add = Thm.global_cterm_of @{theory} @{const plus (real)}
+ val mk_uminus = Thm.apply (Thm.cterm_of @{context} @{const uminus (real)})
+ val add = Thm.cterm_of @{context} @{const plus (real)}
val real0 = Numeral.mk_cnumber @{ctyp real} 0
- val mk_sub = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const minus (real)})
- val mk_mul = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const times (real)})
- val mk_div = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const divide (real)})
- val mk_lt = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less (real)})
- val mk_le = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less_eq (real)})
+ val mk_sub = Thm.mk_binop (Thm.cterm_of @{context} @{const minus (real)})
+ val mk_mul = Thm.mk_binop (Thm.cterm_of @{context} @{const times (real)})
+ val mk_div = Thm.mk_binop (Thm.cterm_of @{context} @{const divide (real)})
+ val mk_lt = Thm.mk_binop (Thm.cterm_of @{context} @{const less (real)})
+ val mk_le = Thm.mk_binop (Thm.cterm_of @{context} @{const less_eq (real)})
fun z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
| z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) cts = SOME (mk_nary add real0 cts)
--- a/src/HOL/Tools/SMT/smt_solver.ML Fri Mar 06 23:44:51 2015 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Fri Mar 06 23:44:57 2015 +0100
@@ -207,7 +207,7 @@
else oracle ()
| (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat)))
- val cfalse = Thm.global_cterm_of @{theory} @{prop False}
+ val cfalse = Thm.cterm_of @{context} @{prop False}
in
fun add_solver ({name, class, avail, command, options, smt_options, default_max_relevant, outcome,
--- a/src/HOL/Tools/SMT/smt_util.ML Fri Mar 06 23:44:51 2015 +0100
+++ b/src/HOL/Tools/SMT/smt_util.ML Fri Mar 06 23:44:57 2015 +0100
@@ -194,7 +194,7 @@
val dest_all_cbinders = repeat_yield (try o dest_cbinder)
-val mk_cprop = Thm.apply (Thm.global_cterm_of @{theory} @{const Trueprop})
+val mk_cprop = Thm.apply (Thm.cterm_of @{context} @{const Trueprop})
fun dest_cprop ct =
(case Thm.term_of ct of
--- a/src/HOL/Tools/SMT/z3_interface.ML Fri Mar 06 23:44:51 2015 +0100
+++ b/src/HOL/Tools/SMT/z3_interface.ML Fri Mar 06 23:44:57 2015 +0100
@@ -112,13 +112,13 @@
| mk_builtin_num ctxt i T =
chained_mk_builtin_num ctxt (get_mk_builtins ctxt) i T
-val mk_true = Thm.global_cterm_of @{theory} (@{const Not} $ @{const False})
-val mk_false = Thm.global_cterm_of @{theory} @{const False}
-val mk_not = Thm.apply (Thm.global_cterm_of @{theory} @{const Not})
-val mk_implies = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const HOL.implies})
-val mk_iff = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const HOL.eq (bool)})
-val conj = Thm.global_cterm_of @{theory} @{const HOL.conj}
-val disj = Thm.global_cterm_of @{theory} @{const HOL.disj}
+val mk_true = Thm.cterm_of @{context} (@{const Not} $ @{const False})
+val mk_false = Thm.cterm_of @{context} @{const False}
+val mk_not = Thm.apply (Thm.cterm_of @{context} @{const Not})
+val mk_implies = Thm.mk_binop (Thm.cterm_of @{context} @{const HOL.implies})
+val mk_iff = Thm.mk_binop (Thm.cterm_of @{context} @{const HOL.eq (bool)})
+val conj = Thm.cterm_of @{context} @{const HOL.conj}
+val disj = Thm.cterm_of @{context} @{const HOL.disj}
fun mk_nary _ cu [] = cu
| mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
@@ -139,15 +139,15 @@
let val cTs = Thm.dest_ctyp (Thm.ctyp_of_cterm array)
in Thm.apply (Thm.mk_binop (SMT_Util.instTs cTs update) array index) value end
-val mk_uminus = Thm.apply (Thm.global_cterm_of @{theory} @{const uminus (int)})
-val add = Thm.global_cterm_of @{theory} @{const plus (int)}
+val mk_uminus = Thm.apply (Thm.cterm_of @{context} @{const uminus (int)})
+val add = Thm.cterm_of @{context} @{const plus (int)}
val int0 = Numeral.mk_cnumber @{ctyp int} 0
-val mk_sub = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const minus (int)})
-val mk_mul = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const times (int)})
-val mk_div = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const z3div})
-val mk_mod = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const z3mod})
-val mk_lt = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less (int)})
-val mk_le = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less_eq (int)})
+val mk_sub = Thm.mk_binop (Thm.cterm_of @{context} @{const minus (int)})
+val mk_mul = Thm.mk_binop (Thm.cterm_of @{context} @{const times (int)})
+val mk_div = Thm.mk_binop (Thm.cterm_of @{context} @{const z3div})
+val mk_mod = Thm.mk_binop (Thm.cterm_of @{context} @{const z3mod})
+val mk_lt = Thm.mk_binop (Thm.cterm_of @{context} @{const less (int)})
+val mk_le = Thm.mk_binop (Thm.cterm_of @{context} @{const less_eq (int)})
fun mk_builtin_fun ctxt sym cts =
(case (sym, cts) of