changeset 45666 | d83797ef0d2d |
parent 43839 | 93f6f24010c2 |
child 46897 | ec793befc232 |
--- a/src/Pure/General/binding.ML Mon Nov 28 20:39:08 2011 +0100 +++ b/src/Pure/General/binding.ML Mon Nov 28 22:05:32 2011 +0100 @@ -122,7 +122,7 @@ (* print *) fun pretty (Binding {prefix, qualifier, name, pos, ...}) = - Pretty.markup (Position.markup pos Markup.binding) + Pretty.markup (Position.markup pos Isabelle_Markup.binding) [Pretty.str (Long_Name.implode (map #1 (prefix @ qualifier) @ [name]))] |> Pretty.quote;