diff -r 56cf1249ee20 -r bf5fcc65586b src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Sun Apr 17 16:36:47 2016 +0200 +++ b/src/HOL/Tools/typedef.ML Sun Apr 17 20:11:02 2016 +0200 @@ -177,7 +177,7 @@ type bindings = {Rep_name: binding, Abs_name: binding, type_definition_name: binding}; fun prefix_binding prfx name = - Binding.reset_pos (Binding.qualified false (prfx ^ Binding.name_of name) name); + Binding.reset_pos (Binding.qualify_name false name (prfx ^ Binding.name_of name)); fun qualify_binding name = Binding.qualify false (Binding.name_of name);