# HG changeset patch
# User wenzelm
# Date 1520343665 -3600
# Node ID 6411290b9d348e01c2fc5f7a3eec4f078eafc265
# Parent  f95a163c58bbfac30a97e19d59a4c69fe2befe9d
eliminated dead code from 2a1acc88a180 (presumably left over from ML type-inference experimentation);

diff -r f95a163c58bb -r 6411290b9d34 src/HOL/Tools/inductive.ML
--- 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;