# 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));