# HG changeset patch # User wenzelm # Date 1451316624 -3600 # Node ID a2d4742b127fff1aa3a87d60bb1f3c91fd692577 # Parent d9acd750c1f636ed7aa6ef1a2e4ddd77e56eaee7 suppress irrelevant position reports; diff -r d9acd750c1f6 -r a2d4742b127f src/Pure/General/binding.ML --- a/src/Pure/General/binding.ML Mon Dec 28 16:29:39 2015 +0100 +++ b/src/Pure/General/binding.ML Mon Dec 28 16:30:24 2015 +0100 @@ -16,6 +16,7 @@ val make: bstring * Position.T -> binding val pos_of: binding -> Position.T val set_pos: Position.T -> binding -> binding + val reset_pos: binding -> binding val name: bstring -> binding val name_of: binding -> bstring val map_name: (bstring -> bstring) -> binding -> binding @@ -84,6 +85,7 @@ fun set_pos pos = map_binding (fn (restricted, concealed, prefix, qualifier, name, _) => (restricted, concealed, prefix, qualifier, name, pos)); +val reset_pos = set_pos Position.none; fun name name = make (name, Position.none); fun name_of (Binding {name, ...}) = name; diff -r d9acd750c1f6 -r a2d4742b127f src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Mon Dec 28 16:29:39 2015 +0100 +++ b/src/Pure/Isar/specification.ML Mon Dec 28 16:30:24 2015 +0100 @@ -242,7 +242,7 @@ error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^ Position.here (Binding.pos_of b)); in (b, mx) end); - val name = Thm.def_binding_optional b raw_name; + val name = Binding.reset_pos (Thm.def_binding_optional b raw_name); val ((lhs, (_, raw_th)), lthy2) = lthy |> Local_Theory.define_internal (var, ((Binding.suffix_name "_raw" name, []), rhs));