--- a/Nominal/nominal_induct.ML	Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_induct.ML	Thu Jul 09 02:32:46 2015 +0100
@@ -57,7 +57,7 @@
       end;
      val substs =
        map2 subst insts concls |> flat |> distinct (op =)
-       |> map (pairself (Thm.cterm_of (Proof_Context.theory_of ctxt)));
+       |> map (apply2 (Thm.cterm_of ctxt));
   in 
     (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) 
   end;
@@ -86,9 +86,6 @@
 
 fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts =
   let
-    val thy = Proof_Context.theory_of ctxt;
-    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_ctxt))) defs;
 
@@ -99,7 +96,7 @@
 
     fun rule_cases ctxt r =
       let val r' = if simp then Induct.simplified_rule ctxt r else r
-      in Rule_Cases.make_nested (Thm.prop_of r') (Induct.rulified_term r') end;
+      in Rule_Cases.make_nested ctxt (Thm.prop_of r') (Induct.rulified_term ctxt r') end;
   in
     (fn i => fn st =>
       rules
@@ -110,7 +107,7 @@
           (CONJUNCTS (ALLGOALS
             let
               val adefs = nth_list atomized_defs (j - 1);
-              val frees = fold (Term.add_frees o prop_of) adefs [];
+              val frees = fold (Term.add_frees o Thm.prop_of) adefs [];
               val xs = nth_list fixings (j - 1);
               val k = nth concls (j - 1) + more_consumes
             in
@@ -131,7 +128,7 @@
                 (Tactic.rtac (rename_params_rule false [] rule') i THEN
                   PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
     THEN_ALL_NEW_CASES
-      ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
+      ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac ctxt)
         else K all_tac)
        THEN_ALL_NEW Induct.rulify_tac ctxt)
   end;
@@ -176,9 +173,8 @@
   Scan.lift (Args.mode Induct.no_simpN) -- 
     (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
       avoiding -- fixing -- rule_spec) >>
-  (fn (no_simp, (((x, y), z), w)) => fn ctxt =>
-    RAW_METHOD_CASES (fn facts =>
-      HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts)));
+  (fn (no_simp, (((x, y), z), w)) => fn ctxt => fn facts =>
+    HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts));
 
 end