diff -r b7b80d5640bb -r 780b7a2c50b6 Nominal/nominal_induct.ML
--- a/Nominal/nominal_induct.ML	Mon Oct 14 11:23:18 2013 +0200
+++ b/Nominal/nominal_induct.ML	Sun Dec 15 15:14:40 2013 +1100
@@ -90,7 +90,7 @@
     val cert = Thm.cterm_of thy;
 
     val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
-    val atomized_defs = map (map (Conv.fconv_rule Induct.atomize_cterm)) defs;
+    val atomized_defs = map (map (Conv.fconv_rule (Induct.atomize_cterm defs_ctxt))) defs;
 
     val finish_rule =
       split_all_tuples defs_ctxt
@@ -104,7 +104,7 @@
     (fn i => fn st =>
       rules
       |> inst_mutual_rule ctxt insts avoiding
-      |> Rule_Cases.consume (flat defs) facts
+      |> Rule_Cases.consume ctxt (flat defs) facts
       |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
         (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
           (CONJUNCTS (ALLGOALS
@@ -122,10 +122,10 @@
                  else
                    Induct.arbitrary_tac defs_ctxt k xs)
             end)
-          THEN' Induct.inner_atomize_tac) j))
-        THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' =>
+          THEN' Induct.inner_atomize_tac ctxt) j))
+        THEN' Induct.atomize_tac ctxt) i st |> Seq.maps (fn st' =>
             Induct.guess_instance ctxt
-              (finish_rule (Induct.internalize more_consumes rule)) i st'
+              (finish_rule (Induct.internalize ctxt more_consumes rule)) i st'
             |> Seq.maps (fn rule' =>
               CASES (rule_cases ctxt rule' cases)
                 (Tactic.rtac (rename_params_rule false [] rule') i THEN
@@ -133,7 +133,7 @@
     THEN_ALL_NEW_CASES
       ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
         else K all_tac)
-       THEN_ALL_NEW Induct.rulify_tac)
+       THEN_ALL_NEW Induct.rulify_tac ctxt)
   end;