author | wenzelm |
Sat, 05 Mar 2016 13:25:41 +0100 | |
changeset 62515 | e73644de5db8 |
parent 62514 | aae510e9a698 |
child 62516 | 5732f1c31566 |
--- 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);