src/HOL/Nominal/nominal_induct.ML

--- a/src/HOL/Nominal/nominal_induct.ML	Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Tue Mar 03 19:08:04 2015 +0100
@@ -54,7 +54,7 @@
       end;
      val substs =
        map2 subst insts concls |> flat |> distinct (op =)
-       |> map (apply2 (Thm.cterm_of (Proof_Context.theory_of ctxt)));
+       |> map (apply2 (Proof_Context.cterm_of ctxt));
   in 
     (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) 
   end;