--- a/src/HOL/Nominal/nominal_inductive.ML Fri Jan 10 16:55:37 2014 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Fri Jan 10 17:44:41 2014 +0100
@@ -343,19 +343,19 @@
map (fold_rev (NominalDatatype.mk_perm [])
(rev pis' @ pis)) params' @ [z])) ihyp;
fun mk_pi th =
- Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm id_apply}]
+ Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]
addsimprocs [NominalDatatype.perm_simproc])
- (Simplifier.simplify (put_simpset eqvt_ss ctxt)
+ (Simplifier.simplify (put_simpset eqvt_ss ctxt')
(fold_rev (mk_perm_bool o cterm_of thy)
(rev pis' @ pis) th));
val (gprems1, gprems2) = split_list
(map (fn (th, t) =>
if null (preds_of ps t) then (SOME th, mk_pi th)
else
- (map_thm ctxt (split_conj (K o I) names)
+ (map_thm ctxt' (split_conj (K o I) names)
(etac conjunct1 1) monos NONE th,
- mk_pi (the (map_thm ctxt (inst_conj_all names ps (rev pis''))
- (inst_conj_all_tac ctxt (length pis'')) monos (SOME t) th))))
+ mk_pi (the (map_thm ctxt' (inst_conj_all names ps (rev pis''))
+ (inst_conj_all_tac ctxt' (length pis'')) monos (SOME t) th))))
(gprems ~~ oprems)) |>> map_filter I;
val vc_compat_ths' = map (fn th =>
let
@@ -625,9 +625,9 @@
in error ("Could not prove equivariance for introduction rule\n" ^
Syntax.string_of_term ctxt''' t ^ "\n" ^ s)
end;
- val res = SUBPROOF (fn {prems, params, ...} =>
+ val res = SUBPROOF (fn {context = ctxt'', prems, params, ...} =>
let
- val prems' = map (fn th => the_default th (map_thm ctxt'
+ val prems' = map (fn th => the_default th (map_thm ctxt''
(split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems;
val prems'' = map (fn th => Simplifier.simplify eqvt_simpset
(mk_perm_bool (cterm_of thy pi) th)) prems';
--- a/src/HOL/Nominal/nominal_inductive2.ML Fri Jan 10 16:55:37 2014 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Jan 10 17:44:41 2014 +0100
@@ -335,13 +335,13 @@
(map Bound (length pTs - 1 downto 0));
val _ $ (f $ (_ $ pi $ l) $ r) = prop_of th2
val th2' =
- Goal.prove ctxt [] []
+ Goal.prove ctxt' [] []
(Logic.list_all (map (pair "pi") pTs, HOLogic.mk_Trueprop
(f $ fold_rev (NominalDatatype.mk_perm (rev pTs))
(pis1 @ pi :: pis2) l $ r)))
(fn _ => cut_facts_tac [th2] 1 THEN
- full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps perm_set_forget) 1) |>
- Simplifier.simplify (put_simpset eqvt_ss ctxt)
+ full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps perm_set_forget) 1) |>
+ Simplifier.simplify (put_simpset eqvt_ss ctxt')
in
(freshs @ [term_of cx],
ths1 @ ths, ths2 @ [th1], ths3 @ [th2'], ctxt')
@@ -401,16 +401,16 @@
(map (fold_rev (NominalDatatype.mk_perm [])
(pis' @ pis) #> cterm_of thy) params' @ [cterm_of thy z]);
fun mk_pi th =
- Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm id_apply}]
+ Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]
addsimprocs [NominalDatatype.perm_simproc])
- (Simplifier.simplify (put_simpset eqvt_ss ctxt)
+ (Simplifier.simplify (put_simpset eqvt_ss ctxt')
(fold_rev (mk_perm_bool o cterm_of thy)
(pis' @ pis) th));
val gprems2 = map (fn (th, t) =>
if null (preds_of ps t) then mk_pi th
else
- mk_pi (the (map_thm ctxt (inst_conj_all names ps (rev pis''))
- (inst_conj_all_tac ctxt (length pis'')) monos (SOME t) th)))
+ mk_pi (the (map_thm ctxt' (inst_conj_all names ps (rev pis''))
+ (inst_conj_all_tac ctxt' (length pis'')) monos (SOME t) th)))
(gprems ~~ oprems);
val perm_freshs_freshs' = map (fn (th, (_, T)) =>
th RS the (AList.lookup op = perm_freshs_freshs T))