diff -r eb4ddd18d635 -r cb495c4807b3 src/HOL/Tools/inductive_set.ML
--- 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));