--- a/src/HOL/Tools/inductive_set.ML Mon Apr 25 16:09:26 2016 +0200
+++ b/src/HOL/Tools/inductive_set.ML Mon Apr 25 16:54:48 2016 +0200
@@ -469,7 +469,7 @@
val (defs, lthy2) = lthy1
|> fold_map Local_Theory.define
(map (fn (((b, mx), (fs, U, _)), p) =>
- ((b, mx), ((Binding.reset_pos (Thm.def_binding b), []),
+ ((b, mx), ((Thm.def_binding b, []),
fold_rev lambda params (HOLogic.Collect_const U $
HOLogic.mk_ptupleabs fs U HOLogic.boolT (list_comb (p, params3))))))
(cnames_syn ~~ cs_info ~~ preds));