# HG changeset patch # User wenzelm # Date 1433230804 -7200 # Node ID cb8828b859a15759c95bd7da3170b6e451a83dc4 # Parent aebfbcab1eb8bb72c49ff45d90ddd9995401cac8 clarified context; diff -r aebfbcab1eb8 -r cb8828b859a1 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Tue Jun 02 09:16:19 2015 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Tue Jun 02 09:40:04 2015 +0200 @@ -120,8 +120,8 @@ val perm_simproc = Simplifier.simproc_global @{theory} "perm_simp" ["pi1 \ (pi2 \ x)"] perm_simproc'; -fun projections rule = - Project_Rule.projections (Proof_Context.init_global (Thm.theory_of_thm rule)) rule +fun projections ctxt rule = + Project_Rule.projections ctxt rule |> map (Drule.export_without_context #> Rule_Cases.save rule); val supp_prod = @{thm supp_prod}; @@ -1114,7 +1114,9 @@ val (_, thy9) = thy8 |> Sign.add_path big_name |> Global_Theory.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] ||>> - Global_Theory.add_thmss [((Binding.name "inducts", projections dt_induct), [case_names_induct])] ||> + Global_Theory.add_thmss + [((Binding.name "inducts", projections (Proof_Context.init_global thy8) dt_induct), + [case_names_induct])] ||> Sign.parent_path ||>> Old_Datatype_Aux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>> Old_Datatype_Aux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>> @@ -1412,7 +1414,9 @@ Sign.add_path big_name |> Global_Theory.add_thms [((Binding.name "strong_induct'", induct_aux), [])] ||>> Global_Theory.add_thms [((Binding.name "strong_induct", induct), [case_names_induct])] ||>> - Global_Theory.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])]; + Global_Theory.add_thmss + [((Binding.name "strong_inducts", projections (Proof_Context.init_global thy9) induct), + [case_names_induct])]; (**** recursion combinator ****) diff -r aebfbcab1eb8 -r cb8828b859a1 src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Tue Jun 02 09:16:19 2015 +0200 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Tue Jun 02 09:40:04 2015 +0200 @@ -145,10 +145,11 @@ val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename; fun inst_fresh vars params i st = let val vars' = Misc_Legacy.term_vars (Thm.prop_of st); - val thy = Thm.theory_of_thm st; in case subtract (op =) vars vars' of [x] => - Seq.single (Thm.instantiate ([], [(Thm.global_cterm_of thy x, Thm.global_cterm_of thy (fold_rev Term.abs params (Bound 0)))]) st) + Seq.single + (Thm.instantiate ([], + [apply2 (Thm.cterm_of ctxt) (x, fold_rev Term.abs params (Bound 0))]) st) | _ => error "fresh_fun_simp: Too many variables, please report." end in diff -r aebfbcab1eb8 -r cb8828b859a1 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Tue Jun 02 09:16:19 2015 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Tue Jun 02 09:40:04 2015 +0200 @@ -39,8 +39,8 @@ fun mk_perm_bool pi th = th RS Drule.cterm_instantiate [(perm_boolI_pi, pi)] perm_boolI; -fun mk_perm_bool_simproc names = Simplifier.simproc_global_i - (Thm.theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn ctxt => +fun mk_perm_bool_simproc names = + Simplifier.simproc_global_i @{theory} "perm_bool" [@{term "perm pi x"}] (fn ctxt => fn Const (@{const_name Nominal.perm}, _) $ _ $ t => if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t)) then SOME perm_bool else NONE diff -r aebfbcab1eb8 -r cb8828b859a1 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Tue Jun 02 09:16:19 2015 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Tue Jun 02 09:40:04 2015 +0200 @@ -43,8 +43,8 @@ fun mk_perm_bool pi th = th RS Drule.cterm_instantiate [(perm_boolI_pi, pi)] perm_boolI; -fun mk_perm_bool_simproc names = Simplifier.simproc_global_i - (Thm.theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn ctxt => +fun mk_perm_bool_simproc names = + Simplifier.simproc_global_i @{theory} "perm_bool" [@{term "perm pi x"}] (fn ctxt => fn Const (@{const_name Nominal.perm}, _) $ _ $ t => if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t)) then SOME perm_bool else NONE diff -r aebfbcab1eb8 -r cb8828b859a1 src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Tue Jun 02 09:16:19 2015 +0200 +++ b/src/HOL/Nominal/nominal_permeq.ML Tue Jun 02 09:40:04 2015 +0200 @@ -70,11 +70,6 @@ val perm_aux_fold = @{thm "perm_aux_fold"}; val supports_fresh_rule = @{thm "supports_fresh"}; -(* pulls out dynamically a thm via the proof state *) -fun dynamic_thms st name = Global_Theory.get_thms (Thm.theory_of_thm st) name; -fun dynamic_thm st name = Global_Theory.get_thm (Thm.theory_of_thm st) name; - - (* needed in the process of fully simplifying permutations *) val strong_congs = [@{thm "if_cong"}] (* needed to avoid warnings about overwritten congs *) @@ -146,7 +141,7 @@ ("general simplification of permutations", fn st => SUBGOAL (fn _ => let val ctxt' = ctxt - addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms) + addsimps (maps (Proof_Context.get_thms ctxt) dyn_thms @ eqvt_thms) addsimprocs [perm_simproc_fun, perm_simproc_app] |> fold Simplifier.del_cong weak_congs |> fold Simplifier.add_cong strong_congs @@ -296,7 +291,6 @@ case Envir.eta_contract (Logic.strip_assums_concl (Thm.term_of goal)) of _ $ (Const (@{const_name finite}, _) $ (Const (@{const_name Nominal.supp}, T) $ x)) => let - val cert = Thm.global_cterm_of (Thm.theory_of_thm st); val ps = Logic.strip_params (Thm.term_of goal); val Ts = rev (map snd ps); val vs = collect_vars 0 x []; @@ -310,8 +304,8 @@ val _ $ (_ $ S $ _) = Logic.strip_assums_concl (hd (Thm.prems_of supports_rule')); val supports_rule'' = Drule.cterm_instantiate - [(cert (head_of S), cert s')] supports_rule' - val fin_supp = dynamic_thms st ("fin_supp") + [apply2 (Thm.cterm_of ctxt) (head_of S, s')] supports_rule' + val fin_supp = Proof_Context.get_thms ctxt "fin_supp" val ctxt' = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp in (tactical ctxt ("guessing of the right supports-set", @@ -332,15 +326,14 @@ fun fresh_guess_tac_i tactical ctxt i st = let val goal = nth (cprems_of st) (i - 1) - val fin_supp = dynamic_thms st ("fin_supp") - val fresh_atm = dynamic_thms st ("fresh_atm") + val fin_supp = Proof_Context.get_thms ctxt "fin_supp" + val fresh_atm = Proof_Context.get_thms ctxt "fresh_atm" val ctxt1 = ctxt addsimps [Thm.symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm val ctxt2 = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp in case Logic.strip_assums_concl (Thm.term_of goal) of _ $ (Const (@{const_name Nominal.fresh}, Type ("fun", [T, _])) $ _ $ t) => let - val cert = Thm.global_cterm_of (Thm.theory_of_thm st); val ps = Logic.strip_params (Thm.term_of goal); val Ts = rev (map snd ps); val vs = collect_vars 0 t []; @@ -354,7 +347,7 @@ val _ $ (_ $ S $ _) = Logic.strip_assums_concl (hd (Thm.prems_of supports_fresh_rule')); val supports_fresh_rule'' = Drule.cterm_instantiate - [(cert (head_of S), cert s')] supports_fresh_rule' + [apply2 (Thm.cterm_of ctxt) (head_of S, s')] supports_fresh_rule' in (tactical ctxt ("guessing of the right set that supports the goal", (EVERY [compose_tac ctxt (false, supports_fresh_rule'', 3) i,