# HG changeset patch
# User wenzelm
# Date 1451316866 -3600
# Node ID cbd310584cff6266be8f0a9135ff7c1821dbd10b
# Parent  a2d4742b127fff1aa3a87d60bb1f3c91fd692577
clarified position information;

diff -r a2d4742b127f -r cbd310584cff src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Mon Dec 28 16:30:24 2015 +0100
+++ b/src/HOL/Tools/inductive.ML	Mon Dec 28 16:34:26 2015 +0100
@@ -843,18 +843,22 @@
 
     val rec_binding =
       if Binding.is_empty alt_name then
-        Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
+        (case cnames_syn of
+          [(b, _)] => b
+        | _ => Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn)))
       else alt_name;
     val rec_name = Binding.name_of rec_binding;
 
     val inductive_defs = Config.get lthy inductive_defs;
+    fun cond_def_binding b =
+      if inductive_defs then Binding.reset_pos (Thm.def_binding b)
+      else Binding.empty;
 
     val ((rec_const, (_, fp_def)), lthy') = lthy
       |> is_auxiliary ? Proof_Context.concealed
       |> Local_Theory.define
-        ((rec_binding, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
-         ((if inductive_defs then Thm.def_binding rec_binding else Binding.empty,
-           @{attributes [nitpick_unfold]}),
+        ((rec_binding, case cnames_syn of [(_, mx)] => mx | _ => NoSyn),
+         ((cond_def_binding rec_binding, @{attributes [nitpick_unfold]}),
            fold_rev lambda params
              (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
       ||> Proof_Context.restore_naming lthy;
@@ -863,15 +867,16 @@
         (Thm.cterm_of lthy' (list_comb (rec_const, params)));
     val specs =
       if is_auxiliary then
-        map_index (fn (i, (name_mx, c)) =>
+        map_index (fn (i, ((b, mx), c)) =>
           let
             val Ts = arg_types_of (length params) c;
             val xs =
               map Free (Variable.variant_frees lthy' intr_ts (mk_names "x" (length Ts) ~~ Ts));
           in
-            (name_mx, (Attrib.empty_binding, fold_rev lambda (params @ xs)
-              (list_comb (rec_const, params @ make_bool_args' bs i @
-                make_args argTs (xs ~~ Ts)))))
+            ((b, mx),
+              ((cond_def_binding b, []), fold_rev lambda (params @ xs)
+                (list_comb (rec_const, params @ make_bool_args' bs i @
+                  make_args argTs (xs ~~ Ts)))))
           end) (cnames_syn ~~ cs)
       else [];
     val (consts_defs, lthy'') = lthy'
diff -r a2d4742b127f -r cbd310584cff src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Mon Dec 28 16:30:24 2015 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Mon Dec 28 16:34:26 2015 +0100
@@ -470,10 +470,11 @@
     (* define inductive sets using previously defined predicates *)
     val (defs, lthy2) = lthy1
       |> fold_map Local_Theory.define
-        (map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []),
-           fold_rev lambda params (HOLogic.Collect_const U $
-             HOLogic.mk_ptupleabs fs U HOLogic.boolT (list_comb (p, params3))))))
-           (cnames_syn ~~ cs_info ~~ preds));
+        (map (fn (((b, mx), (fs, U, _)), p) =>
+          ((b, mx), ((Binding.reset_pos (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));
 
     (* prove theorems for converting predicate to set notation *)
     val lthy3 = fold