--- 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