# HG changeset patch # User wenzelm # Date 1425681897 -3600 # Node ID 5980e75a204e53ab5519733aff687b36daedc045 # Parent 34030d67afb9c937d049bf4f76fb342b35c377ea clarified context; diff -r 34030d67afb9 -r 5980e75a204e src/HOL/Tools/ATP/atp_problem_generate.ML --- 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 diff -r 34030d67afb9 -r 5980e75a204e src/HOL/Tools/ATP/atp_util.ML --- 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 diff -r 34030d67afb9 -r 5980e75a204e src/HOL/Tools/Meson/meson.ML --- 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 diff -r 34030d67afb9 -r 5980e75a204e src/HOL/Tools/Meson/meson_clausify.ML --- 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}) diff -r 34030d67afb9 -r 5980e75a204e src/HOL/Tools/Metis/metis_reconstruct.ML --- 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 => diff -r 34030d67afb9 -r 5980e75a204e src/HOL/Tools/Metis/metis_tactic.ML --- 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 diff -r 34030d67afb9 -r 5980e75a204e src/HOL/Tools/SMT/smt_normalize.ML --- 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"}) diff -r 34030d67afb9 -r 5980e75a204e src/HOL/Tools/SMT/smt_real.ML --- 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) diff -r 34030d67afb9 -r 5980e75a204e src/HOL/Tools/SMT/smt_solver.ML --- 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, diff -r 34030d67afb9 -r 5980e75a204e src/HOL/Tools/SMT/smt_util.ML --- 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 diff -r 34030d67afb9 -r 5980e75a204e src/HOL/Tools/SMT/z3_interface.ML --- 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