# HG changeset patch # User wenzelm # Date 1457180741 -3600 # Node ID e73644de5db87a2947a068f699559bf1139d09a4 # Parent aae510e9a698c3fd494ee71459413d9297e53a20 avoid spam in position reports; diff -r aae510e9a698 -r e73644de5db8 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);