--- a/src/HOL/Nominal/nominal_induct.ML Sun Jul 26 20:54:02 2015 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Sun Jul 26 20:56:44 2015 +0200
@@ -54,9 +54,9 @@
end;
val substs =
map2 subst insts concls |> flat |> distinct (op =)
- |> map (apply2 (Thm.cterm_of ctxt));
+ |> map (fn (t, u) => (#1 (dest_Var t), Thm.cterm_of ctxt u));
in
- (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule)
+ (((cases, nconcls), consumes), infer_instantiate ctxt substs joined_rule)
end;
fun rename_params_rule internal xs rule =