src/HOL/Tools/ATP/atp_util.ML
changeset 48902 44a6967240b7
parent 48766 553ad5f99968
child 49982 724cfe013182
--- a/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 23 12:55:23 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 23 13:03:29 2012 +0200
@@ -84,7 +84,7 @@
       | strip_c_style_comment (_ :: cs) accum = strip_c_style_comment cs accum
     and strip_spaces_in_list _ [] accum = accum
       | strip_spaces_in_list true (#"%" :: cs) accum =
-        strip_spaces_in_list true (cs |> chop_while (not_equal #"\n") |> snd)
+        strip_spaces_in_list true (cs |> take_prefix (not_equal #"\n") |> snd)
                              accum
       | strip_spaces_in_list true (#"/" :: #"*" :: cs) accum =
         strip_c_style_comment cs accum