eliminated dead code from 2a1acc88a180 (presumably left over from ML type-inference experimentation);
--- a/src/HOL/Tools/inductive.ML Sun Mar 04 20:09:09 2018 +0100
+++ b/src/HOL/Tools/inductive.ML Tue Mar 06 14:41:05 2018 +0100
@@ -1194,7 +1194,6 @@
val ps = map Free pnames;
val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn');
- val _ = map (fn abbr => Local_Defs.fixed_abbrev abbr ctxt2) abbrevs;
val ctxt3 = ctxt2 |> fold (snd oo Local_Defs.fixed_abbrev) abbrevs;
val expand = Assumption.export_term ctxt3 lthy #> Proof_Context.cert_term lthy;