avoid spam in position reports;
authorwenzelm
Sat, 05 Mar 2016 13:25:41 +0100
changeset 62515 e73644de5db8
parent 62514 aae510e9a698
child 62516 5732f1c31566
avoid spam in position reports;
src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Sat Mar 05 12:49:47 2016 +0100
+++ b/src/HOL/Tools/typedef.ML	Sat Mar 05 13:25:41 2016 +0100
@@ -177,7 +177,7 @@
 type bindings = {Rep_name: binding, Abs_name: binding, type_definition_name: binding};
 
 fun prefix_binding prfx name =
-  Binding.qualified false (prfx ^ Binding.name_of name) name;
+  Binding.reset_pos (Binding.qualified false (prfx ^ Binding.name_of name) name);
 
 fun qualify_binding name = Binding.qualify false (Binding.name_of name);