diff -r ee0881a54c72 -r 3d6ac2f68bf3 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Dec 16 17:18:52 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Dec 16 17:58:31 2013 +0100
@@ -231,8 +231,7 @@
 val dummy_phi = AAtom (ATerm (("", []), []))
 val dummy_inference = Inference_Source ("", [])
 
-(* "skip_term" is there to cope with Waldmeister nonsense such as
-   "theory(equality)". *)
+(* "skip_term" is there to cope with Waldmeister nonsense such as "theory(equality)". *)
 fun parse_dependency x =
   (parse_inference_source >> snd
    || scan_general_id --| skip_term >> single) x