# HG changeset patch # User wenzelm # Date 1425681205 -3600 # Node ID 0d77c51b5040155c4420b4bba37874c0df211f85 # Parent 2b15625b85fc331653d51f3f52e5df8a80c6eef5 clarified context; diff -r 2b15625b85fc -r 0d77c51b5040 src/HOL/Decision_Procs/approximation_generator.ML --- a/src/HOL/Decision_Procs/approximation_generator.ML Fri Mar 06 23:14:41 2015 +0100 +++ b/src/HOL/Decision_Procs/approximation_generator.ML Fri Mar 06 23:33:25 2015 +0100 @@ -117,7 +117,7 @@ } fun rewrite_with ctxt thms = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps thms) -fun conv_term thy conv r = Thm.global_cterm_of thy r |> conv |> Thm.prop_of |> Logic.dest_equals |> snd +fun conv_term ctxt conv r = Thm.cterm_of ctxt r |> conv |> Thm.prop_of |> Logic.dest_equals |> snd fun approx_random ctxt prec eps frees e xs genuine_only size seed = let @@ -138,7 +138,7 @@ (AList.lookup op = (map dest_Free xs ~~ ts) #> the_default Term.dummy #> curry op $ @{term "real::float\_"} - #> conv_term (Proof_Context.theory_of ctxt) (rewrite_with ctxt postproc_form_eqs)) + #> conv_term ctxt (rewrite_with ctxt postproc_form_eqs)) frees in if approximate ctxt (mk_approx_form e ts) |> is_True @@ -159,13 +159,12 @@ "\ (p \ q) \ \ p \ \ q" "\ (p \ q) \ \ p \ \ q" "\ \ q \ q" - by auto - } + by auto} fun reify_goal ctxt t = HOLogic.mk_not t - |> conv_term (Proof_Context.theory_of ctxt) (rewrite_with ctxt preproc_form_eqs) - |> conv_term (Proof_Context.theory_of ctxt) (Reification.conv ctxt form_equations) + |> conv_term ctxt (rewrite_with ctxt preproc_form_eqs) + |> conv_term ctxt (Reification.conv ctxt form_equations) |> dest_interpret_form ||> HOLogic.dest_list diff -r 2b15625b85fc -r 0d77c51b5040 src/HOL/Decision_Procs/commutative_ring_tac.ML --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Fri Mar 06 23:14:41 2015 +0100 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Fri Mar 06 23:33:25 2015 +0100 @@ -76,12 +76,11 @@ fun reif_eq ctxt (eq as Const (@{const_name HOL.eq}, Type (@{type_name fun}, [T, _])) $ lhs $ rhs) = if Sign.of_sort (Proof_Context.theory_of ctxt) (T, cr_sort) then let - val thy = Proof_Context.theory_of ctxt; val fs = Misc_Legacy.term_frees eq; - val cvs = Thm.global_cterm_of thy (HOLogic.mk_list T fs); - val clhs = Thm.global_cterm_of thy (reif_polex T fs lhs); - val crhs = Thm.global_cterm_of thy (reif_polex T fs rhs); - val ca = Thm.global_ctyp_of thy T; + val cvs = Thm.cterm_of ctxt (HOLogic.mk_list T fs); + val clhs = Thm.cterm_of ctxt (reif_polex T fs lhs); + val crhs = Thm.cterm_of ctxt (reif_polex T fs rhs); + val ca = Thm.ctyp_of ctxt T; in (ca, cvs, clhs, crhs) end else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort ctxt cr_sort) | reif_eq _ _ = error "reif_eq: not an equation"; diff -r 2b15625b85fc -r 0d77c51b5040 src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Fri Mar 06 23:14:41 2015 +0100 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Fri Mar 06 23:33:25 2015 +0100 @@ -40,7 +40,6 @@ fun linz_tac ctxt q = Object_Logic.atomize_prems_tac ctxt THEN' SUBGOAL (fn (g, i) => let - val thy = Proof_Context.theory_of ctxt; (* Transform the term*) val (t, np, nh) = prepare_for_linz q g; (* Some simpsets for dealing with mod div abs and nat*) @@ -73,7 +72,7 @@ |> fold Simplifier.add_cong @{thms conj_le_cong imp_le_cong} (* simp rules for elimination of abs *) val simpset3 = put_simpset HOL_basic_ss ctxt |> Splitter.add_split @{thm abs_split} - val ct = Thm.global_cterm_of thy (HOLogic.mk_Trueprop t) + val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t) (* Theorem for the nat --> int transformation *) val pre_thm = Seq.hd (EVERY [simp_tac mod_div_simpset 1, simp_tac simpset0 1, @@ -86,7 +85,7 @@ (case Thm.prop_of pre_thm of Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => let - val pth = linzqe_oracle (Thm.global_cterm_of thy (Envir.eta_long [] t1)) + val pth = linzqe_oracle (Thm.cterm_of ctxt (Envir.eta_long [] t1)) in ((pth RS iffD2) RS pre_thm, assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)) diff -r 2b15625b85fc -r 0d77c51b5040 src/HOL/Decision_Procs/ferrack_tac.ML --- a/src/HOL/Decision_Procs/ferrack_tac.ML Fri Mar 06 23:14:41 2015 +0100 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Fri Mar 06 23:33:25 2015 +0100 @@ -50,12 +50,11 @@ THEN' (REPEAT_DETERM o split_tac ctxt [@{thm split_min}, @{thm split_max}, @{thm abs_split}]) THEN' SUBGOAL (fn (g, i) => let - val thy = Proof_Context.theory_of ctxt (* Transform the term*) val (t,np,nh) = prepare_for_linr q g (* Some simpsets for dealing with mod div abs and nat*) val simpset0 = put_simpset HOL_basic_ss ctxt addsimps comp_arith - val ct = Thm.global_cterm_of thy (HOLogic.mk_Trueprop t) + val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t) (* Theorem for the nat --> int transformation *) val pre_thm = Seq.hd (EVERY [simp_tac simpset0 1, diff -r 2b15625b85fc -r 0d77c51b5040 src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Fri Mar 06 23:14:41 2015 +0100 +++ b/src/HOL/Decision_Procs/mir_tac.ML Fri Mar 06 23:33:25 2015 +0100 @@ -70,7 +70,6 @@ THEN' (REPEAT_DETERM o split_tac ctxt [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]) THEN' SUBGOAL (fn (g, i) => let - val thy = Proof_Context.theory_of ctxt (* Transform the term*) val (t,np,nh) = prepare_for_mir q g (* Some simpsets for dealing with mod div abs and nat*) @@ -101,7 +100,7 @@ @{thm "int_0"}, @{thm "int_1"}] |> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}] (* simp rules for elimination of abs *) - val ct = Thm.global_cterm_of thy (HOLogic.mk_Trueprop t) + val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t) (* Theorem for the nat --> int transformation *) val pre_thm = Seq.hd (EVERY [simp_tac mod_div_simpset 1, simp_tac simpset0 1, @@ -116,8 +115,8 @@ let val pth = (* If quick_and_dirty then run without proof generation as oracle*) if Config.get ctxt quick_and_dirty - then mirfr_oracle (false, Thm.global_cterm_of thy (Envir.eta_long [] t1)) - else mirfr_oracle (true, Thm.global_cterm_of thy (Envir.eta_long [] t1)) + then mirfr_oracle (false, Thm.cterm_of ctxt (Envir.eta_long [] t1)) + else mirfr_oracle (true, Thm.cterm_of ctxt (Envir.eta_long [] t1)) in ((pth RS iffD2) RS pre_thm, assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))