--- a/src/HOL/Nominal/nominal_inductive2.ML Tue Jun 04 20:01:02 2019 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Tue Jun 04 20:49:33 2019 +0200
@@ -169,7 +169,8 @@
(Induct.lookup_inductP ctxt (hd names)))));
val induct_cases' = if null induct_cases then replicate (length intrs) ""
else induct_cases;
- val ([raw_induct'], ctxt') = Variable.import_terms false [Thm.prop_of raw_induct] ctxt;
+ val (raw_induct', ctxt') = ctxt
+ |> yield_singleton (Variable.import_terms false) (Thm.prop_of raw_induct);
val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb);
val ps = map (fst o snd) concls;