diff -r b7b80d5640bb -r 780b7a2c50b6 Nominal/nominal_dt_quot.ML
--- a/Nominal/nominal_dt_quot.ML	Mon Oct 14 11:23:18 2013 +0200
+++ b/Nominal/nominal_dt_quot.ML	Sun Dec 15 15:14:40 2013 +1100
@@ -338,7 +338,7 @@
         end)
   in
     induct_prove qtys (goals1 @ goals2) qinduct tac ctxt
-    |> map atomize
+    |> map (atomize ctxt)
     |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms fun_eq_iff[symmetric]}))
   end
 
@@ -591,14 +591,14 @@
             (* for freshness conditions *) 
             val tac1 = SOLVED' (EVERY'
               [ simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps peqs),
-                rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}),
+                rewrite_goal_tac ctxt'' (@{thms fresh_star_Un[THEN eq_reflection]}),
                 conj_tac (DETERM o resolve_tac fprops') ]) 
 
             (* for equalities between constructors *)
             val tac2 = SOLVED' (EVERY' 
               [ rtac (@{thm ssubst} OF prems),
-                rewrite_goal_tac (map safe_mk_equiv eq_iff_thms),
-                rewrite_goal_tac (map safe_mk_equiv abs_eqs),
+                rewrite_goal_tac ctxt'' (map safe_mk_equiv eq_iff_thms),
+                rewrite_goal_tac ctxt'' (map safe_mk_equiv abs_eqs),
                 conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ]) 
 
             (* proves goal "P" *)