src/Tools/Code/code_printer.ML
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 =