# HG changeset patch
# User wenzelm
# Date 1461596088 -7200
# Node ID cb495c4807b31cd1011da6ec9a0aeac95d6d8477
# Parent  eb4ddd18d635fbaf601fef499914f92182e65c77
clarified def binding position: reset for implicit/derived binding, keep for explicit binding;

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));
diff -r eb4ddd18d635 -r cb495c4807b3 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Apr 25 16:09:26 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Apr 25 16:54:48 2016 +0200
@@ -746,7 +746,7 @@
       #-> (fn rhss =>
         let
           val defs = (vars ~~ (name_atts ~~ rhss)) |> map (fn ((x, mx), ((a, atts), rhs)) =>
-            ((x, mx), ((Binding.reset_pos (Thm.def_binding_optional x a), atts), rhs)));
+            ((x, mx), ((Thm.def_binding_optional x a, atts), rhs)));
         in map_context_result (Local_Defs.add_defs defs) end))
     |-> (set_facts o map (#2 o #2))
   end;
@@ -936,7 +936,7 @@
       |> unflat (map snd raw_defs);
     val notes =
       map2 (fn ((a, raw_atts), _) => fn def_thms =>
-        ((Binding.reset_pos (Thm.def_binding_optional (Binding.conglomerate (map #1 def_thms)) a),
+        ((Thm.def_binding_optional (Binding.conglomerate (map #1 def_thms)) a,
           map (prep_att defs_ctxt) raw_atts), map (fn (_, th) => ([th], [])) def_thms))
         raw_defs def_thmss;
   in
diff -r eb4ddd18d635 -r cb495c4807b3 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Mon Apr 25 16:09:26 2016 +0200
+++ b/src/Pure/Isar/specification.ML	Mon Apr 25 16:54:48 2016 +0200
@@ -249,7 +249,7 @@
               error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
                 Position.here (Binding.pos_of b));
           in (b, mx) end);
-    val name = Binding.reset_pos (Thm.def_binding_optional b raw_name);
+    val name = Thm.def_binding_optional b raw_name;
     val ((lhs, (_, raw_th)), lthy2) = lthy
       |> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));
 
diff -r eb4ddd18d635 -r cb495c4807b3 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon Apr 25 16:09:26 2016 +0200
+++ b/src/Pure/more_thm.ML	Mon Apr 25 16:54:48 2016 +0200
@@ -566,13 +566,9 @@
 fun def_name_optional c "" = def_name c
   | def_name_optional _ name = name;
 
-val def_binding = Binding.map_name def_name;
-
-fun def_binding_optional b name =
-  if Binding.is_empty name then def_binding b else name;
-
-fun make_def_binding cond b =
-  if cond then Binding.reset_pos (def_binding b) else Binding.empty;
+val def_binding = Binding.map_name def_name #> Binding.reset_pos;
+fun def_binding_optional b name = if Binding.is_empty name then def_binding b else name;
+fun make_def_binding cond b = if cond then def_binding b else Binding.empty;
 
 
 (* unofficial theorem names *)