suppress irrelevant position reports;

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

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