--- a/src/HOL/Nominal/nominal_inductive.ML Thu Sep 13 18:11:59 2007 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Thu Sep 13 23:58:38 2007 +0200
@@ -147,7 +147,7 @@
InductivePackage.the_inductive ctxt (Sign.intern_const thy s);
val raw_induct = atomize_induct raw_induct;
val monos = InductivePackage.get_monos ctxt;
- val eqvt_thms = NominalThmDecls.get_eqvt_thms thy;
+ val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
val _ = (case names \\ foldl (apfst prop_of #> add_term_consts) [] eqvt_thms of
[] => ()
| xs => error ("Missing equivariance theorem for predicate(s): " ^
@@ -461,7 +461,7 @@
end;
val perm_pi_simp = PureThy.get_thms thy (Name "perm_pi_simp");
val eqvt_ss = HOL_basic_ss addsimps
- (NominalThmDecls.get_eqvt_thms thy @ perm_pi_simp) addsimprocs
+ (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
[mk_perm_bool_simproc names];
val t = Logic.unvarify (concl_of raw_induct);
val pi = Name.variant (add_term_names (t, [])) "pi";