clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
--- 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));
--- 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
--- 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));
--- 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 *)