--- 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 \<bullet> (pi2 \<bullet> 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 ****)
--- 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
--- 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
--- 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
--- 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,