| changeset 47576 | b32aae03e3d6 |
| parent 46949 | 94aa7b81bcf6 |
| child 48072 | ace701efe203 |
--- a/src/Tools/Code/code_printer.ML Thu Apr 19 08:45:13 2012 +0200 +++ b/src/Tools/Code/code_printer.ML Thu Apr 19 10:16:51 2012 +0200 @@ -146,7 +146,7 @@ |> pair false; fun filter (XML.Elem (name_attrs, xs)) = fold (if is_selected name_attrs then add_content_with_space else filter) xs - | filter (XML.Text s) = I; + | filter (XML.Text _) = I; in snd (fold filter tree (true, Buffer.empty)) end; fun format presentation_names width =