1.1 --- a/src/Tools/Code/code_printer.ML	Thu Apr 19 08:45:13 2012 +0200
     1.2 +++ b/src/Tools/Code/code_printer.ML	Thu Apr 19 10:16:51 2012 +0200
     1.3 @@ -146,7 +146,7 @@
     1.4            |> pair false;
     1.5          fun filter (XML.Elem (name_attrs, xs)) =
     1.6                fold (if is_selected name_attrs then add_content_with_space else filter) xs
     1.7 -          | filter (XML.Text s) = I;
     1.8 +          | filter (XML.Text _) = I;
     1.9        in snd (fold filter tree (true, Buffer.empty)) end;
    1.10  
    1.11  fun format presentation_names width =